Information for RPM idris-1.3.4-1.ocs23.aarch64.rpm
ID | 139665 | |||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Name | idris | |||||||||||||||||||||||||||
Version | 1.3.4 | |||||||||||||||||||||||||||
Release | 1.ocs23 | |||||||||||||||||||||||||||
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-07-22 04:19:39 GMT | |||||||||||||||||||||||||||
Size | 32.38 MB | |||||||||||||||||||||||||||
d9d40b1caa3b0c7670ca8d203ac9f7ea | ||||||||||||||||||||||||||||
License | BSD-3-Clause | |||||||||||||||||||||||||||
Buildroot | dist-ocs23-epol9-build-214505-15918 | |||||||||||||||||||||||||||
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 |