Changelog of @hackage/idris 0.1.7

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