git.iko.soy/Idris-dev
on master help sign in
Prelude.Nat: add decision procedure for IsSucc
42783aeMichael Morgan
libs/prelude/Prelude/Nat.idr+8
compare with master
unifiedsplit
@@ -43,6 +43,14 @@ isSucc (S n) = True
43data IsSucc : (n : Nat) -> Type where
43data IsSucc : (n : Nat) -> Type where
44 ItIsSucc : IsSucc (S n)
44 ItIsSucc : IsSucc (S n)
45
45
46+Uninhabited (IsSucc Z) where
47+ uninhabited ItIsSucc impossible
48+
49+||| A decision procedure for `IsSucc`
50+isItSucc : (n : Nat) -> Dec (IsSucc n)
51+isItSucc Z = No absurd
52+isItSucc (S n) = Yes ItIsSucc
53+
46--------------------------------------------------------------------------------
54--------------------------------------------------------------------------------
47-- Basic arithmetic functions
55-- Basic arithmetic functions
48--------------------------------------------------------------------------------
56--------------------------------------------------------------------------------