The idris package

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.


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.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,,, 0.10, 0.10.1, 0.10.2, 0.10.3, 0.11, 0.11.1, 0.11.2, 0.12, 0.12.1, 0.12.2, 0.12.3, 0.99, 0.99.1, 0.99.2, 1.0
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:39:57 UTC 2013 by EdwinBrady


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