@@ -13,17 +13,29 @@ specified precisely in the type. It is compiled, with eager
13evaluation. Its features are influenced by Haskell and ML.
13evaluation. Its features are influenced by Haskell and ML.
15+ Full dependent types with dependent pattern matching
15+ Full dependent types with dependent pattern matching
16+ Simple case expressions, where-clauses, with-rule
17+ Simple case expressions, where-clauses, with-rule
17+ Pattern matching let- and lambda-bindings
19+ Pattern matching let- and lambda-bindings
18+ Overloading via Interfaces (Type class-like), Monad comprehensions
21+ Overloading via Interfaces (Type class-like), Monad comprehensions
19+ do-notation, idiom brackets
23+ do-notation, idiom brackets
20+ Syntactic conveniences for lists, tuples, dependent pairs
25+ Syntactic conveniences for lists, tuples, dependent pairs
21+ Totality checking
27+ Totality checking
22+ Coinductive types
29+ Coinductive types
23+ Indentation significant syntax, Extensible syntax
31+ Indentation significant syntax, Extensible syntax
24+ Tactic based theorem proving (influenced by Coq)
33+ Tactic based theorem proving (influenced by Coq)
25+ Cumulative universes
35+ Cumulative universes
26+ Simple Foreign Function Interface
37+ Simple Foreign Function Interface
27+ Hugs style interactive environment
39+ Hugs style interactive environment
29It is important to note that Idris is first and foremost a research tool
41It is important to note that Idris is first and foremost a research tool