Changelog for idris-0.1.7.1
If this renders badly as markdown, see the plain text version
New in 0.1.6
- Changed dependent pair syntax to <| x, y |> so that << and >> can be
integer shift operators.
- Removed '#' as type of types (must use 'Set' now).
- searchcontext tactic
- equalities.idr in the library
- codata keyword
- proof and tryproof keywords for invoking a decision procedure in a
- Syntactic sugar for Cons lists
- Lots of smaller changes and bug fixes
New in 0.1.5
- Changed '#' to Set for the type of types
- old syntax works, but is deprecated and will be removed soon.
- 'syntax' definitions
- %spec works in pattern clauses as well as CAFs
- Added 'Proof' type for marking computationally irrelevant terms.
- Added List permutation proofs to the library (perm.idr)
- Various new functions in the library.
- Lots of bug fixes
New in 0.1.4