Functional Programming Language with Dependent Types
Idris is a general purpose language with full dependent types. It is compiled, with eager evaluation. Dependent types allow types to be predicated on values, meaning that some aspects of a program's behaviour can be specified precisely in the type. The language is closely related to Epigram and Agda. There is a tutorial at <https://www.idris-lang.org/documentation>. Features include: * Full, first class, dependent types with dependent pattern matching * where clauses, with rule, case expressions, pattern matching let and lambda bindings * Interfaces (similar to type classes), monad comprehensions * do notation, idiom brackets, syntactic conveniences for lists, tuples, dependent pairs * Totality checking * Coinductive types * Indentation significant syntax, extensible syntax * Cumulative universes * Simple foreign function interface (to C) * Hugs style interactive environment.
Release | Stable | Testing |
---|---|---|
Fedora Rawhide | 1.3.4-2.fc36 | - |
Fedora 35 | 1.3.3-6.20210626git2ef8238d0.fc35 | - |
Fedora 34 | 1.3.3-3.fc34 | - |
EPEL 7 | 0.9.9.1-2.el7 | - |
You can contact the maintainers of this package via email at
idris dash maintainers at fedoraproject dot org
.