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]).