@@ -43,6 +43,14 @@ isSucc (S n) = True
4343data IsSucc : (n : Nat) -> Type where
4444 ItIsSucc : IsSucc (S n)
4545
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+
4654--------------------------------------------------------------------------------
4755-- Basic arithmetic functions
4856--------------------------------------------------------------------------------