git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4106 from msmorgan/feature/isSucc

Prelude.Nat: add IsSucc predicate type

commit7081ff0381ef51d139faf04d7fdeb25b83b16ff6 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateMon 9 Oct 2017, 09:46 (9 years ago) parent4304a0a7b9be7e
2 files changed+14
compare with master
unifiedsplit
CHANGELOG.md+1 libs/prelude/Prelude/Nat.idr+13
CHANGELOG.md+1
@@ -14,6 +14,7 @@
1414+ Added `Text.Literate`, a module for working with literate source files.
1515+ Added `Data.IORef`, for working with mutable references in `IO` and `JS_IO`.
1616+ Added `discriminate` and `construct` tactics to Pruviloj.
17++ Added `IsSucc` type to `Prelude`, which proves that a `Nat` is a successor.
1718
1819## Tool Updates
1920+ Private functions are no longer visible in the REPL except for modules
libs/prelude/Prelude/Nat.idr+13
@@ -38,6 +38,19 @@ 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+
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+
4154--------------------------------------------------------------------------------
4255-- Basic arithmetic functions
4356--------------------------------------------------------------------------------