From da9880d5b446fdb8a0ff68bdca8463082b9e20f2 Mon Sep 17 00:00:00 2001 From: Zoe Stafford <36511192+Z-snails@users.noreply.github.com> Date: Mon, 1 Jan 2024 15:08:47 +0000 Subject: [PATCH] Update libs/prelude/Prelude/Types.idr Co-authored-by: Mathew Polzin --- libs/prelude/Prelude/Types.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libs/prelude/Prelude/Types.idr b/libs/prelude/Prelude/Types.idr index 6ff12e4cbd..4db366940e 100644 --- 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