@@ -18,12 +18,12 @@ Description: Idris is a general purpose language with full dependent types.
1818 <http://www.idris-lang.org/documentation>.
1919 Features include:
2020 .
21− * Full dependent types with dependent pattern matching
21+ * Full, first class, dependent types with dependent pattern matching
2222 .
23− * where clauses, with rule, simple case expressions,
23+ * where clauses, with rule, case expressions,
2424 pattern matching let and lambda bindings
2525 .
26− * Type classes, monad comprehensions
26+ * Interfaces (similar to type classes), monad comprehensions
2727 .
2828 * do notation, idiom brackets, syntactic conveniences for lists,
2929 tuples, dependent pairs
@@ -34,8 +34,6 @@ Description: Idris is a general purpose language with full dependent types.
3434 .
3535 * Indentation significant syntax, extensible syntax
3636 .
37− * Tactic based theorem proving (influenced by Coq)
38− .
3937 * Cumulative universes
4038 .
4139 * Simple foreign function interface (to C)