git.iko.soy/Idris-dev
on master help sign in
add CHANGELOG entry for IsSucc
7b9be7eMichael Morgan
CHANGELOG.md+1
compare with master
unifiedsplit
@@ -14,6 +14,7 @@
14+ Added `Text.Literate`, a module for working with literate source files.
14+ Added `Text.Literate`, a module for working with literate source files.
15+ Added `Data.IORef`, for working with mutable references in `IO` and `JS_IO`.
15+ Added `Data.IORef`, for working with mutable references in `IO` and `JS_IO`.
16+ Added `discriminate` and `construct` tactics to Pruviloj.
16+ Added `discriminate` and `construct` tactics to Pruviloj.
17++ Added `IsSucc` type to `Prelude`, which proves that a `Nat` is a successor.
17
18
18## Tool Updates
19## Tool Updates
19+ Private functions are no longer visible in the REPL except for modules
20+ Private functions are no longer visible in the REPL except for modules