Information for RPM idris-1.3.4-1.oc9.aarch64.rpm
ID | 221644 | |||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Name | idris | |||||||||||||||||||||||||||
Version | 1.3.4 | |||||||||||||||||||||||||||
Release | 1.oc9 | |||||||||||||||||||||||||||
Epoch | ||||||||||||||||||||||||||||
Arch | aarch64 | |||||||||||||||||||||||||||
Summary | Functional Programming Language with Dependent Types | |||||||||||||||||||||||||||
Description | 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. | |||||||||||||||||||||||||||
Build Time | 2024-08-05 05:36:12 GMT | |||||||||||||||||||||||||||
Size | 32.38 MB | |||||||||||||||||||||||||||
488a0fc827c175f955d3cfe227d36311 | ||||||||||||||||||||||||||||
License | BSD-3-Clause | |||||||||||||||||||||||||||
Buildroot | dist-oc9-epol-build-92309-59299 | |||||||||||||||||||||||||||
Provides |
|
|||||||||||||||||||||||||||
Obsoletes | No Obsoletes | |||||||||||||||||||||||||||
Conflicts | No Conflicts | |||||||||||||||||||||||||||
Requires |
|
|||||||||||||||||||||||||||
Recommends | No Recommends | |||||||||||||||||||||||||||
Suggests | No Suggests | |||||||||||||||||||||||||||
Supplements | No Supplements | |||||||||||||||||||||||||||
Enhances | No Enhances | |||||||||||||||||||||||||||
Files | ||||||||||||||||||||||||||||
Component of | No Buildroots |