git.iko.soy/Idris-dev
on master help sign in
Prelude.Nat: add IsSucc predicate type
92ed2d7Michael Morgan
libs/prelude/Prelude/Nat.idr+5
compare with master
unifiedsplit
@@ -38,6 +38,11 @@ total isSucc : Nat -> Bool
38isSucc Z = False
38isSucc Z = False
39isSucc (S n) = True
39isSucc (S n) = True
40
40
41+
42+||| Proof that `n` is not equal to Z
43+data IsSucc : (n : Nat) -> Type where
44+ ItIsSucc : IsSucc (S n)
45+
41--------------------------------------------------------------------------------
46--------------------------------------------------------------------------------
42-- Basic arithmetic functions
47-- Basic arithmetic functions
43--------------------------------------------------------------------------------
48--------------------------------------------------------------------------------