From 14db785ebe58a18fdeda14ac78985ddcfec564af Mon Sep 17 00:00:00 2001 From: Christian Rasmussen Date: Tue, 20 Aug 2019 18:25:52 +0200 Subject: [PATCH] Fixes #88: integerToNat hangs for negative integers --- libs/prelude/Prelude.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr index bbead0d..5c8b571 100644 --- a/libs/prelude/Prelude.idr +++ b/libs/prelude/Prelude.idr @@ -564,7 +564,7 @@ data Nat = Z | S Nat public export integerToNat : Integer -> Nat integerToNat x - = if intToBool (prim__eq_Integer x 0) + = if intToBool (prim__lte_Integer x 0) then Z else S (assert_total (integerToNat (prim__sub_Integer x 1)))