edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-09-20 04:17:38 +03:00
Code Issues Projects Releases Wiki Activity

Fixes #88: integerToNat hangs for negative integers

Browse Source
This commit is contained in:
Christian Rasmussen 2019-08-20 18:25:52 +02:00
parent a87a3c14c2
commit 14db785ebe
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/prelude/Prelude.idr
View File

@ -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)))