Prelude.Nat: add IsSucc predicate type
By popular demand.
commit92ed2d7c5b96e2b2816ba9cda1aca91d2eb52403
authorMichael Morgan <morgan.michael@me.com>
dateSat 7 Oct 2017, 15:35 (9 years ago)
parentc3113e7
libs/prelude/Prelude/Nat.idr+5
@@ -38,6 +38,11 @@ total isSucc : Nat -> Bool
3838isSucc Z = False
3939isSucc (S n) = True
4040
41+
42+||| Proof that `n` is not equal to Z
43+data IsSucc : (n : Nat) -> Type where
44+ ItIsSucc : IsSucc (S n)
45+
4146--------------------------------------------------------------------------------
4247-- Basic arithmetic functions
4348--------------------------------------------------------------------------------