@@ -10,10 +10,32 @@ Stability: Beta
1010Category: Compilers/Interpreters, Dependent Types
1111Synopsis: Dependently Typed Functional Programming Language
1212Description: Idris is a general purpose language with full dependent types.
13+ It is compiled, with eager evaluation.
1314 Dependent types allow types to be predicated on values,
1415 meaning that some aspects of a program's behaviour can be
1516 specified precisely in the type. The language is closely
1617 related to Epigram and Agda. There is a tutorial at <http://www.idris-lang.org/documentation>.
18+ Features include:
19+ .
20+ * Full dependent types with dependent pattern matching
21+ .
22+ * where clauses, with rule, simple case expressions,
23+ pattern matching let and lambda bindings
24+ .
25+ * Type classes, monad comprehensions
26+ .
27+ * do notation, idiom brackets, syntactic conveniences for lists,
28+ tuples, dependent pairs
29+ .
30+ * Indentation significant syntax, extensible syntax
31+ .
32+ * Tactic based theorem proving (influenced by Coq)
33+ .
34+ * Cumulative universes
35+ .
36+ * Simple foreign function interface (to C)
37+ .
38+ * Hugs style interactive environment
1739
1840Cabal-Version: >= 1.6
1941Build-type: Custom