mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-10-27 01:42:29 +03:00
Merge pull request #89 from chrrasmussen/fix-integerToNat
Fixes #88: integerToNat hangs for negative integers
This commit is contained in:
commit
09b13eef21
@ -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)))
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user