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:
- From version 1.23 cabal supports specifiying explicit dependencies for Custom setup scripts. Consider using cabal-version >= 1.23 and adding a 'custom-setup' section with a 'setup-depends' field that specifies the dependencies of the Setup.hs script itself. The 'setup-depends' field uses the same syntax as 'build-depends', so a simple example would be 'setup-depends: base, Cabal'.
- 'ghc-options/ghc-prof-options: -fprof*' profiling flags are typically not appropriate for a distributed library package. These flags are useful to profile this package, but when profiling other packages that use this one these flags clutter the profile output with excessive detail. If you think other packages really want to see cost centres from this package then use '-fprof-auto-exported' which puts cost centres only on exported functions. Alternatively, if you want to use this, make it conditional based on a Cabal configuration flag (with 'manual: True' and 'default: False') and enable that flag during development.
- 'ghc-options/ghc-prof-options: -fprof*' profiling flags are typically not appropriate for a distributed library package. These flags are useful to profile this package, but when profiling other packages that use this one these flags clutter the profile output with excessive detail. If you think other packages really want to see cost centres from this package then use '-fprof-auto-exported' which puts cost centres only on exported functions. Alternatively, if you want to use this, make it conditional based on a Cabal configuration flag (with 'manual: True' and 'default: False') and enable that flag during development.
- 'ghc-options/ghc-prof-options: -fprof*' profiling flags are typically not appropriate for a distributed library package. These flags are useful to profile this package, but when profiling other packages that use this one these flags clutter the profile output with excessive detail. If you think other packages really want to see cost centres from this package then use '-fprof-auto-exported' which puts cost centres only on exported functions. Alternatively, if you want to use this, make it conditional based on a Cabal configuration flag (with 'manual: True' and 'default: False') and enable that flag during development.
- 'ghc-options/ghc-prof-options: -fprof*' profiling flags are typically not appropriate for a distributed library package. These flags are useful to profile this package, but when profiling other packages that use this one these flags clutter the profile output with excessive detail. If you think other packages really want to see cost centres from this package then use '-fprof-auto-exported' which puts cost centres only on exported functions. Alternatively, if you want to use this, make it conditional based on a Cabal configuration flag (with 'manual: True' and 'default: False') and enable that flag during development.
- 'ghc-options/ghc-prof-options: -fprof*' profiling flags are typically not appropriate for a distributed library package. These flags are useful to profile this package, but when profiling other packages that use this one these flags clutter the profile output with excessive detail. If you think other packages really want to see cost centres from this package then use '-fprof-auto-exported' which puts cost centres only on exported functions. Alternatively, if you want to use this, make it conditional based on a Cabal configuration flag (with 'manual: True' and 'default: False') and enable that flag during development.
- 'ghc-options/ghc-prof-options: -fprof*' profiling flags are typically not appropriate for a distributed library package. These flags are useful to profile this package, but when profiling other packages that use this one these flags clutter the profile output with excessive detail. If you think other packages really want to see cost centres from this package then use '-fprof-auto-exported' which puts cost centres only on exported functions. Alternatively, if you want to use this, make it conditional based on a Cabal configuration flag (with 'manual: True' and 'default: False') and enable that flag during development.
- Exposed modules use unallocated top-level names: Idris IRTS 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
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.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.0, 1.1.1, 1.2.0, 1.3.0, 1.3.1, 1.3.2, 1.3.3, 1.3.4 |
---|---|
Change log | CHANGELOG.md |
Dependencies | aeson (>=0.6 && <1.2), annotated-wl-pprint (>=0.7 && <0.8), ansi-terminal (<0.7), ansi-wl-pprint (<0.7), array (>=0.4.0.1 && <0.6), async (<2.2), base (>=4 && <5), base64-bytestring (<1.1), binary (>=0.7 && <0.9), blaze-html (>=0.6.1.3 && <0.10), blaze-markup (>=0.5.2.1 && <0.9), bytestring (<0.11), cheapskate (<0.2), code-page (>=0.1 && <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), fsnotify (>=0.2 && <2.2), haskeline (>=0.7 && <0.8), idris, ieee754 (>=0.7 && <=0.8.0), mintty (>=0.1 && <0.2), mtl (>=2.1 && <2.3), network (<2.7), optparse-applicative (>=0.13 && <0.14), parsers (>=0.9 && <0.13), pretty (<1.2), process (<1.5), regex-tdfa (>=1.2), safe (>=0.3.9), split (<0.3), tagsoup (<0.14.1), terminal-size (<0.4), text (>=1.2.1.0 && <1.3), time (>=1.4 && <1.7), transformers (<0.6), transformers-compat (>=0.3), trifecta (>=1.6 && <1.7), uniplate (>=1.6 && <1.7), unix (<2.8), unordered-containers (<0.3), utf8-string (<1.1), vector (<0.13), vector-binary-instances (<0.3), Win32 (<2.4), zip-archive (>0.2.3.5 && <0.4), zlib (<0.6.1) [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 2017-08-01T12:08:30Z |
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.Info
- Idris.Inliner
- Idris.Interactive
- Idris.Main
- Idris.ModeCommon
- Idris.Options
- Idris.Output
- Idris.Package
- Idris.Parser
- Idris.PartialEval
- Idris.Primitives
- Idris.ProofSearch
- Idris.Prover
- Idris.Providers
- Idris.REPL
- Idris.Reflection
- Idris.Termination
- Idris.Transforms
- Idris.TypeSearch
- Idris.Unlit
- Idris.WhoCalls
- Util
Flags
Manual Flags
Name | Description | Default |
---|---|---|
ffi | Build support for libffi | Disabled |
gmp | Use GMP for Integers | 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-1.1.0.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
Package maintainers
For package maintainers and hackage trustees