idris v0.1.x Release Notes

  • Complete rewrite.

    ๐Ÿ‘‰ User visible changes

    • ๐Ÿ†• New proof/tactics syntax
    • ๐Ÿ†• New syntax for pairs/dependent pairs
    • Indentation-significant syntax
    • โž• Added type classes
    • โž• Added where clauses
    • โž• Added case expressions, pattern matching let and lambda
    • โž• Added monad comprehensions
    • โž• Added cumulativity and universe checking
    • Ad-hoc name overloading
      • Resolved by type or explicit namespace
    • ๐Ÿ’… Modules (Haskell-style)
    • public, abstract and private access to functions and types
    • Separate type-checking
    • ๐Ÿ‘Œ Improved interactive environment
    • Replaced 'do using' with Monad class
    • Extended syntax macros

    Internal changes

    • Everything :-)
    • All definitions (functions, classes and instances) are elaborated to top level, fully explicit, data declarations and pattern matching definitions, which are verified by a minimal type checker.

    ๐Ÿš€ This is the first release of a complete reimplementation. There will be bugs. If you find any, please do not hesitate to contact Edwin Brady ([email protected]).