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