Idris 0.9.0 released

[Edwin Brady]

Dear all,
Idris 0.9.0 has now been released onto hackage. To install, run 'cabal update' then type 'cabal install idris'. Release notes are below, details at http://idris-lang.org/archives/130.

There's a tutorial at http://idris-lang.org/documentation. Have fun :).

Edwin.
=======================================

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
(ec...@st-andrews.ac.uk).

[Cezar Ionescu]

I think you should also post it to the Agda mailing list.

Best,
Cezar.