The idris package

[Tags: bsd3, library, program]

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 Features include:


Versions0.1.3,, 0.1.4, 0.1.5, 0.1.7,, 0.9.0, 0.9.1, 0.9.2,, 0.9.3,, 0.9.4,, 0.9.5,, 0.9.6,, 0.9.7, 0.9.8, 0.9.9,,,, 0.9.10,, 0.9.11,,, 0.9.12, 0.9.13,, 0.9.14,,,, 0.9.15,, 0.9.16, 0.9.17,, 0.9.18,, 0.9.19,, 0.9.20,
Change logNone available
Dependenciesansi-terminal, ansi-wl-pprint, base (==4.*), binary, bytestring, Cabal, containers, deepseq, directory (>=1.2), filepath, haskeline (>=0.7), language-java (>=0.2.6), mtl, network, parsers (==0.9), pretty, process, split, text, time (>=1.4), transformers, trifecta (==1.1), unix, unordered-containers, utf8-string, vector, vector-binary-instances, Win32, xml [details]
AuthorEdwin Brady
MaintainerEdwin Brady <>
CategoryCompilers/Interpreters, Dependent Types
Home page
Source repositoryhead: git clone git://
UploadedThu Nov 28 10:40:32 UTC 2013 by EdwinBrady
DistributionsFedora:, NixOS:
Downloads14259 total (320 in last 30 days)
0 []
StatusDocs not available [build log]
Successful builds reported [all 5 reports]


llvmBuild the LLVM backendDisabledManual
ffiBuild support for libffiDisabledManual
gmpUse GMP for IntegersDisabledManual

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info


Maintainers' corner

For package maintainers and hackage trustees