idris: Functional Programming Language with Dependent Types

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.

[maintain] [Publish]

Warnings:

'ghc-options: -threaded' has no effect for libraries. It should only be used for executables.
'ghc-prof-options: -auto-all' is fine during development, but not recommended in a distributed package. If you want to use this, make it conditional based on a flag (with 'manual: True' and 'default: False') and enable that flag during development.
'ghc-prof-options: -auto-all' is fine during development, but not recommended in a distributed package. If you want to use this, make it conditional based on a flag (with 'manual: True' and 'default: False') and enable that flag during development.
'ghc-prof-options: -auto-all' is fine during development, but not recommended in a distributed package. If you want to use this, make it conditional based on a flag (with 'manual: True' and 'default: False') and enable that flag during development.
'ghc-prof-options: -auto-all' is fine during development, but not recommended in a distributed package. If you want to use this, make it conditional based on a flag (with 'manual: True' and 'default: False') and enable that flag during development.
'ghc-prof-options: -auto-all' is fine during development, but not recommended in a distributed package. If you want to use this, make it conditional based on a flag (with 'manual: True' and 'default: False') and enable that flag during development.
Exposed modules use unallocated top-level names: Idris IRTS Pkg Util

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 http://www.idris-lang.org/documentation. Features include:

Full dependent types with dependent pattern matching
where clauses, with rule, simple case expressions, pattern matching let and lambda bindings
Type classes, monad comprehensions
do notation, idiom brackets, syntactic conveniences for lists, tuples, dependent pairs
Totality checking
Coinductive types
Indentation significant syntax, extensible syntax
Tactic based theorem proving (influenced by Coq)
Cumulative universes
Simple foreign function interface (to C)
Hugs style interactive environment

Properties

Versions	0.1.3, 0.1.3.1, 0.1.4, 0.1.5, 0.1.7, 0.1.7.1, 0.9.0, 0.9.1, 0.9.2, 0.9.2.1, 0.9.3, 0.9.3.1, 0.9.4, 0.9.4.1, 0.9.5, 0.9.5.1, 0.9.6, 0.9.6.1, 0.9.7, 0.9.8, 0.9.9, 0.9.9.1, 0.9.9.2, 0.9.9.3, 0.9.10, 0.9.10.1, 0.9.11, 0.9.11.1, 0.9.11.2, 0.9.12, 0.9.13, 0.9.13.1, 0.9.14, 0.9.14.1, 0.9.14.2, 0.9.14.3, 0.9.15, 0.9.15.1, 0.9.16, 0.9.17, 0.9.17.1, 0.9.18, 0.9.18.1, 0.9.19, 0.9.19, 0.9.19.1, 0.9.20, 0.9.20.1, 0.9.20.2, 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, 1.1.0, 1.1.1, 1.2.0, 1.3.0, 1.3.1, 1.3.2, 1.3.3, 1.3.4
Change log	None available
Dependencies	annotated-wl-pprint (>=0.7 && <0.8), ansi-terminal (<0.7), ansi-wl-pprint (<0.7), base (>=4 && <5), base64-bytestring (<1.1), binary (>=0.7 && <0.8), blaze-html (>=0.6.1.3 && <0.9), blaze-markup (>=0.5.2.1 && <0.8), bytestring (<0.11), cheapskate (<0.2), containers (>=0.5 && <0.6), deepseq (<1.5), directory (>=1.2.2.0 && <1.2.3.0 \|\| >1.2.3.0), filepath (<1.5), fingertree (>=0.1 && <0.2), haskeline (>=0.7 && <0.8), idris, mtl (>=2.1 && <2.3), network (<2.7), optparse-applicative (>=0.11 && <0.12), parsers (>=0.9 && <0.13), pretty (<1.2), process (<1.3), safe, split (<0.3), text (>=1.2.1.0 && <1.3), time (>=1.4 && <1.6), transformers (<0.5), transformers-compat (>=0.3), trifecta (>=1.1 && <1.6), uniplate (>=1.6 && <1.7), unix (<2.8), unordered-containers (<0.3), utf8-string (<=1), vector (<0.11), vector-binary-instances (<0.3), Win32 (<2.4), zip-archive (>0.2.3.5 && <0.2.4), zlib (<0.6) [details]
License	BSD-3-Clause
Author	Edwin Brady
Maintainer	Edwin Brady <eb@cs.st-andrews.ac.uk>
Category	Compilers/Interpreters, Dependent Types
Home page	http://www.idris-lang.org/
Source repo	head: git clone git://github.com/idris-lang/Idris-dev.git
Uploaded	by EdwinBrady at 2015-08-31T19:52:37Z

Modules

[Index]

Flags

Manual Flags

Name	Description	Default
ffi	Build support for libffi	Disabled
gmp	Use GMP for Integers	Disabled
curses	Use Curses to get the screen width	Disabled
release	This is an official release	Enabled
freestanding	Build an Idris that doesn't use cabal	Disabled
ci	Built everything using "-Werror", meant for CI-builds only	Disabled
execonly	Build executables only, skip the libraries and RTS	Disabled

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

Downloads

idris-0.9.19.tar.gz [browse] (Cabal source package)
Package description (as included in the package)

Maintainer's Corner

Package maintainers

EdwinBrady, niklasl

For package maintainers and hackage trustees

edit package information