Update libs/prelude/Prelude/Types.idr

Co-authored-by: Mathew Polzin <[email protected]>
idris-lang · Jan 1, 2024 · da9880d · da9880d
1 parent 504a444
commit da9880d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/libs/prelude/Prelude/Types.idr b/libs/prelude/Prelude/Types.idr
@@ -39,7 +39,7 @@ nonNegativeIntegerToNat :
 nonNegativeIntegerToNat 0 = Z
 nonNegativeIntegerToNat x =
     let -- x >= 0 and x != 0
-        -- so x >= 0 so x - 1 >= 0
+        -- so x > 0 so x - 1 >= 0
         prf = believe_me Refl
      in S $ nonNegativeIntegerToNat {prf}
           $ assert_smaller x $ x - 1