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 term * 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 ------------ * Namespaces