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.
Warnings:
- '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.
- '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, 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
[Skip to Readme]
Properties
Modules
[Index]
- IRTS
- Idris
- Idris.ASTUtils
- Idris.AbsSyntax
- Idris.AbsSyntaxTree
- Idris.Apropos
- Idris.CaseSplit
- Idris.Chaser
- Idris.CmdOptions
- Idris.Colours
- Idris.Completion
- Core
- Idris.Coverage
- Idris.DSL
- Idris.DataOpts
- Idris.DeepSeq
- Idris.Delaborate
- Idris.Directives
- Idris.Docs
- Idris.Docstrings
- Elab
- Idris.ElabDecls
- Idris.Erasure
- Idris.ErrReverse
- Idris.Error
- Idris.Help
- Idris.IBC
- Idris.IdeMode
- Idris.IdrisDoc
- Idris.Imports
- Idris.Inliner
- Idris.Interactive
- Idris.Output
- Idris.Parser
- Idris.PartialEval
- Idris.Primitives
- Idris.ProofSearch
- Idris.Prover
- Idris.Providers
- Idris.REPL
- Idris.Reflection
- Idris.Transforms
- Idris.TypeSearch
- Idris.Unlit
- Idris.WhoCalls
- Pkg
- Util
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.10.1.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
Package maintainers
For package maintainers and hackage trustees