@@ -13,17 +13,29 @@ specified precisely in the type. It is compiled, with eager
1313evaluation. Its features are influenced by Haskell and ML.
1414
1515+ Full dependent types with dependent pattern matching
16+
1617+ Simple case expressions, where-clauses, with-rule
18+
1719+ Pattern matching let- and lambda-bindings
20+
1821+ Overloading via Interfaces (Type class-like), Monad comprehensions
22+
1923+ do-notation, idiom brackets
24+
2025+ Syntactic conveniences for lists, tuples, dependent pairs
26+
2127+ Totality checking
28+
2229+ Coinductive types
30+
2331+ Indentation significant syntax, Extensible syntax
32+
2433+ Tactic based theorem proving (influenced by Coq)
34+
2535+ Cumulative universes
36+
2637+ Simple Foreign Function Interface
38+
2739+ Hugs style interactive environment
2840
2941It is important to note that Idris is first and foremost a research tool