Name: idris Version: 0.9.20.1 License: BSD3 License-file: LICENSE Author: Edwin Brady Maintainer: Edwin Brady Homepage: http://www.idris-lang.org/ Stability: Beta Category: Compilers/Interpreters, Dependent Types Synopsis: Functional Programming Language with Dependent Types Description: 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: . * 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 Cabal-Version: >= 1.8 Build-type: Custom Data-files: idrisdoc/styles.css jsrts/Runtime-browser.js jsrts/Runtime-common.js jsrts/Runtime-node.js jsrts/jsbn/jsbn.js jsrts/jsbn/LICENSE rts/arduino/idris_main.c rts/idris_bitstring.c rts/idris_bitstring.h rts/idris_gc.c rts/idris_gc.h rts/idris_gmp.c rts/idris_gmp.h rts/idris_heap.c rts/idris_heap.h rts/idris_main.c rts/idris_net.c rts/idris_net.h rts/idris_opts.c rts/idris_opts.h rts/idris_rts.c rts/idris_rts.h rts/idris_stats.c rts/idris_stats.h rts/idris_stdfgn.c rts/idris_stdfgn.h rts/mini-gmp.c rts/mini-gmp.h rts/libtest.c Extra-doc-files: CHANGELOG CITATION.md CONTRIBUTING.md CONTRIBUTORS README.md idris-tutorial.pdf man/idris.1 samples/effects/*.idr samples/misc/*.idr samples/misc/*.lidr samples/tutorial/*.idr Extra-source-files: Makefile config.mk stack.yaml rts/*.c rts/*.h rts/arduino/*.c rts/windows/*.c rts/Makefile libs/Makefile libs/prelude/prelude.ipkg libs/prelude/Prelude/*.idr libs/prelude/Decidable/*.idr libs/prelude/Language/*.idr libs/prelude/Language/Reflection/*.idr libs/prelude/Makefile libs/prelude/*.idr libs/base/base.ipkg libs/base/*.idr libs/base/Control/*.idr libs/base/Control/Monad/*.idr libs/base/Data/*.idr libs/base/Data/Vect/*.idr libs/base/Debug/*.idr libs/base/Language/Reflection/*.idr libs/base/Makefile libs/base/System/*.idr libs/base/System/Concurrency/*.idr libs/base/Syntax/*.idr libs/contrib/contrib.ipkg libs/contrib/Makefile libs/contrib/Classes/*.idr libs/contrib/Control/*.idr libs/contrib/Control/Isomorphism/*.idr libs/contrib/Control/Algebra/*.idr libs/contrib/Data/*.idr libs/contrib/Data/Nat/*.idr libs/contrib/Data/Nat/DivMod/*.idr libs/contrib/Data/Matrix/*.idr libs/contrib/Decidable/*.idr libs/contrib/Network/*.idr libs/contrib/System/Concurrency/*.idr libs/effects/Makefile libs/effects/effects.ipkg libs/effects/Effect/*.idr libs/effects/Effect/Logging/*.idr libs/effects/*.idr libs/pruviloj/Makefile libs/pruviloj/pruviloj.ipkg libs/pruviloj/*.idr libs/pruviloj/Pruviloj/*.idr libs/pruviloj/Pruviloj/Derive/*.idr libs/pruviloj/Pruviloj/Internals/*.idr test/Makefile test/runtest.pl test/reg001/run test/reg001/*.idr test/reg001/expected test/reg002/run test/reg002/*.idr test/reg002/expected test/reg003/run test/reg003/*.idr test/reg003/expected test/reg004/run test/reg004/*.idr test/reg004/expected test/reg006/run test/reg006/*.idr test/reg006/expected test/reg007/run test/reg007/*.lidr test/reg007/expected test/reg010/run test/reg010/*.idr test/reg010/expected test/reg013/run test/reg013/*.idr test/reg013/expected test/reg016/run test/reg016/*.idr test/reg016/expected test/reg017/run test/reg017/*.idr test/reg017/expected test/reg018/run test/reg018/*.idr test/reg018/expected test/reg020/run test/reg020/*.idr test/reg020/expected test/reg023/run test/reg023/*.idr test/reg023/expected test/reg024/run test/reg024/*.idr test/reg024/expected test/reg025/run test/reg025/*.idr test/reg025/expected test/reg027/run test/reg027/*.idr test/reg027/expected test/reg028/run test/reg028/*.idr test/reg028/expected test/reg029/run test/reg029/*.idr test/reg029/expected test/reg031/run test/reg031/*.idr test/reg031/expected test/reg032/run test/reg032/*.idr test/reg032/expected test/reg034/run test/reg034/*.idr test/reg034/expected test/reg035/run test/reg035/*.idr test/reg035/*.lidr test/reg035/expected test/reg036/run test/reg036/*.idr test/reg036/expected test/reg037/run test/reg037/*.idr test/reg037/expected test/reg038/run test/reg038/*.idr test/reg038/expected test/reg039/run test/reg039/*.idr test/reg039/expected test/reg040/run test/reg040/*.idr test/reg040/expected test/reg041/run test/reg041/*.idr test/reg041/expected test/reg042/run test/reg042/*.idr test/reg042/expected test/reg044/run test/reg044/*.idr test/reg044/expected test/reg045/run test/reg045/*.idr test/reg045/expected test/reg046/run test/reg046/*.idr test/reg046/expected test/reg047/run test/reg047/*.idr test/reg047/expected test/reg048/run test/reg048/*.idr test/reg048/expected test/reg049/run test/reg049/*.idr test/reg049/expected test/reg050/run test/reg050/*.idr test/reg050/expected test/reg051-disabled/run test/reg051-disabled/*.idr test/reg051-disabled/expected test/reg052/run test/reg052/*.idr test/reg052/expected test/reg053/run test/reg053/*.idr test/reg053/expected test/reg054/run test/reg054/*.idr test/reg054/expected test/reg055/run test/reg055/*.idr test/reg055/expected test/reg056/run test/reg056/*.idr test/reg056/expected test/reg057/run test/reg057/*.idr test/reg057/expected test/reg058/run test/reg058/*.idr test/reg058/expected test/reg059/run test/reg059/*.idr test/reg059/expected test/reg060/run test/reg060/*.idr test/reg060/expected test/reg061/run test/reg061/*.idr test/reg061/expected test/reg062/run test/reg062/*.idr test/reg062/expected test/reg063/run test/reg063/*.idr test/reg063/expected test/reg064/run test/reg064/*.idr test/reg064/expected test/reg065/run test/reg065/*.idr test/reg065/expected test/reg066/run test/reg066/*.idr test/reg066/expected test/basic001/run test/basic001/*.idr test/basic001/expected test/basic002/run test/basic002/*.idr test/basic002/expected test/basic003/run test/basic003/*.idr test/basic003/expected test/basic004/run test/basic004/*.idr test/basic004/expected test/basic005/run test/basic005/*.lidr test/basic005/expected test/basic006/run test/basic006/*.idr test/basic006/expected test/basic007/run test/basic007/*.idr test/basic007/expected test/basic008/run test/basic008/*.idr test/basic008/expected test/basic009/run test/basic009/*.idr test/basic009/expected test/basic009/B/*.idr test/basic010/run test/basic010/*.idr test/basic010/expected test/basic011/run test/basic011/*.idr test/basic011/expected test/basic012/run test/basic012/*.idr test/basic012/expected test/basic013/run test/basic013/*.idr test/basic013/expected test/basic014/run test/basic014/*.idr test/basic014/expected test/basic015/run test/basic015/*.idr test/basic015/expected test/basic016/run test/basic016/*.idr test/basic016/expected test/bignum001/run test/bignum001/*.idr test/bignum001/expected test/bignum002/run test/bignum002/*.idr test/bignum002/expected test/classes001/*.idr test/classes001/run test/classes001/expected test/classes001/input test/corecords001/*.idr test/corecords001/run test/corecords001/expected test/corecords002/*.idr test/corecords002/run test/corecords002/expected test/delab001/*.idr test/delab001/run test/delab001/expected test/delab001/input test/disambig002/run test/disambig002/*.idr test/disambig002/expected test/dsl001/run test/dsl001/*.idr test/dsl001/expected test/dsl002/run test/dsl002/test test/dsl002/*.idr test/dsl002/expected test/dsl003/run test/dsl003/*.idr test/dsl003/expected test/dsl004/run test/dsl004/*.idr test/dsl004/expected test/effects001/run test/effects001/*.idr test/effects001/expected test/effects001/testFile test/effects002/run test/effects002/*.idr test/effects002/expected test/effects003/run test/effects003/*.idr test/effects003/expected test/effects003/input test/effects004/run test/effects004/*.idr test/effects004/expected test/effects004/input test/effects005/run test/effects005/*.idr test/effects005/expected test/error001/run test/error001/*.idr test/error001/expected test/error002/run test/error002/*.idr test/error002/expected test/error003/run test/error003/*.idr test/error003/expected test/error004/run test/error004/*.idr test/error004/expected test/error005/run test/error005/*.idr test/error005/expected test/ffi001/run test/ffi001/*.idr test/ffi001/expected test/ffi002/run test/ffi002/*.idr test/ffi002/expected test/ffi003/run test/ffi003/*.idr test/ffi003/expected test/ffi003/input test/ffi004/run test/ffi004/*.idr test/ffi004/theType test/ffi004/theOtherType test/ffi004/expected test/ffi005/*.idr test/ffi005/run test/ffi005/expected test/ffi006/*.idr test/ffi006/*.c test/ffi006/run test/ffi006/expected test/folding001/*.idr test/folding001/run test/folding001/expected test/idrisdoc001/run test/idrisdoc001/expected test/idrisdoc001/*.idr test/idrisdoc001/*.ipkg test/idrisdoc002/run test/idrisdoc002/expected test/idrisdoc002/*.idr test/idrisdoc002/*.ipkg test/idrisdoc003/run test/idrisdoc003/expected test/idrisdoc003/*.idr test/idrisdoc003/*.ipkg test/idrisdoc004/run test/idrisdoc004/expected test/idrisdoc004/*.idr test/idrisdoc004/*.ipkg test/idrisdoc005/run test/idrisdoc005/expected test/idrisdoc005/*.idr test/idrisdoc005/*.ipkg test/idrisdoc006/run test/idrisdoc006/expected test/idrisdoc006/A/fully/Qualified/NAME.idr test/idrisdoc006/*.idr test/idrisdoc006/*.ipkg test/idrisdoc007/run test/idrisdoc007/expected test/idrisdoc007/*.idr test/idrisdoc007/*.ipkg test/idrisdoc008/run test/idrisdoc008/expected test/idrisdoc008/*.idr test/idrisdoc008/*.ipkg test/idrisdoc009/run test/idrisdoc009/expected test/idrisdoc009/input test/idrisdoc009/*.idr test/interactive001/run test/interactive001/input test/interactive001/*.idr test/interactive001/expected test/interactive002/run test/interactive002/input test/interactive002/*.idr test/interactive002/expected test/interactive003/run test/interactive003/input test/interactive003/*.idr test/interactive003/expected test/interactive004/run test/interactive004/input test/interactive004/*.idr test/interactive004/expected test/interactive005/run test/interactive005/input test/interactive005/*.idr test/interactive005/expected test/interactive006/run test/interactive006/input test/interactive006/*.idr test/interactive006/expected test/interactive007/run test/interactive007/input test/interactive007/expected test/interactive008/run test/interactive008/input test/interactive008/expected test/interactive009/run test/interactive009/input test/interactive009/*.idr test/interactive009/expected test/interactive010/expected test/interactive010/input test/interactive010/run test/interactive011/expected test/interactive011/input test/interactive011/run test/interactive011/*.idr test/interactive012/expected test/interactive012/input test/interactive012/run test/interactive012/*.idr test/io001/run test/io001/*.idr test/io001/expected test/io002/run test/io002/*.idr test/io002/expected test/io003/run test/io003/*.idr test/io003/expected test/literate001/run test/literate001/*.lidr test/literate001/expected test/meta001/run test/meta001/*.idr test/meta001/expected test/meta002/run test/meta002/*.idr test/meta002/expected test/primitives001/run test/primitives001/*.idr test/primitives001/expected test/primitives001/input test/primitives002/run test/primitives002/expected test/primitives003/run test/primitives003/*.idr test/primitives003/expected test/pkg001/run test/pkg001/test.ipkg test/pkg001/*.idr test/pkg001/expected test/proof001/run test/proof001/*.idr test/proof001/expected test/proof002/run test/proof002/*.idr test/proof002/expected test/proof003/run test/proof003/*.idr test/proof003/expected test/proof004/run test/proof004/*.idr test/proof004/expected test/proof005/run test/proof005/*.idr test/proof005/expected test/proof006/run test/proof006/*.idr test/proof006/expected test/proof007/run test/proof007/*.idr test/proof007/expected test/proof008/run test/proof008/*.idr test/proof008/expected test/proof009/run test/proof009/*.idr test/proof009/expected test/proof009/input test/proof010/run test/proof010/*.idr test/proof010/expected test/proofsearch001/run test/proofsearch001/*.idr test/proofsearch001/expected test/proofsearch002/run test/proofsearch002/*.idr test/proofsearch002/expected test/proofsearch003/run test/proofsearch003/*.idr test/proofsearch003/expected test/pruviloj001/run test/pruviloj001/*.idr test/pruviloj001/expected test/quasiquote001/run test/quasiquote001/*.idr test/quasiquote001/expected test/quasiquote002/run test/quasiquote002/*.idr test/quasiquote002/expected test/quasiquote003/run test/quasiquote003/*.idr test/quasiquote003/expected test/quasiquote004/run test/quasiquote004/*.idr test/quasiquote004/expected test/quasiquote005/run test/quasiquote005/*.idr test/quasiquote005/expected test/quasiquote006/run test/quasiquote006/*.idr test/quasiquote006/expected test/records001/run test/records001/*.idr test/records001/expected test/records002/run test/records002/*.idr test/records002/expected test/records003/run test/records003/*.idr test/records003/expected test/sourceLocation001/run test/sourceLocation001/*.idr test/sourceLocation001/expected test/sugar001/run test/sugar001/*.idr test/sugar001/expected test/sugar002/run test/sugar002/*.idr test/sugar002/expected test/sugar003/run test/sugar003/*.idr test/sugar003/expected test/sugar004/run test/sugar004/*.idr test/sugar004/expected test/sugar005/run test/sugar005/*.idr test/sugar005/expected test/syntax001/run test/syntax001/*.idr test/syntax001/expected test/syntax002/run test/syntax002/*.idr test/syntax002/expected test/tactics001/run test/tactics001/*.idr test/tactics001/expected test/totality001/run test/totality001/*.idr test/totality001/expected test/totality002/run test/totality002/*.idr test/totality002/expected test/totality003/run test/totality003/*.idr test/totality003/expected test/totality004/run test/totality004/*.idr test/totality004/expected test/totality005/run test/totality005/*.idr test/totality005/expected test/totality006/run test/totality006/*.idr test/totality006/expected test/totality007/run test/totality007/*.ipkg test/totality007/src/*.idr test/totality007/expected test/totality008/run test/totality008/*.idr test/totality008/expected test/totality009/run test/totality009/*.idr test/totality009/expected test/totality010/run test/totality010/*.idr test/totality010/expected test/tutorial001/run test/tutorial001/*.idr test/tutorial001/expected test/tutorial002/run test/tutorial002/*.idr test/tutorial002/expected test/tutorial003/run test/tutorial003/*.idr test/tutorial003/expected test/tutorial004/run test/tutorial004/*.idr test/tutorial004/expected test/tutorial005/run test/tutorial005/*.idr test/tutorial005/expected test/tutorial006/run test/tutorial006/*.idr test/tutorial006/expected test/unique001/run test/unique001/*.idr test/unique001/expected test/unique002/run test/unique002/*.idr test/unique002/expected test/unique003/run test/unique003/*.idr test/unique003/expected test/docs001/run test/docs001/input test/docs001/*.idr test/docs001/expected test/docs002/run test/docs002/input test/docs002/*.idr test/docs002/expected test/docs003/run test/docs003/input test/docs003/*.idr test/docs003/expected benchmarks/ALL benchmarks/*.pl benchmarks/README benchmarks/fasta/fasta.idr benchmarks/fasta/fasta.ipkg benchmarks/pidigits/pidigits.idr benchmarks/pidigits/pidigits.ipkg benchmarks/quasigroups/board benchmarks/quasigroups/*.idr benchmarks/quasigroups/qgsolve.ipkg benchmarks/trivial/sortvec.idr benchmarks/trivial/sortvec.ipkg source-repository head type: git location: git://github.com/idris-lang/Idris-dev.git Flag FFI Description: Build support for libffi Default: False manual: True Flag GMP Description: Use GMP for Integers Default: False manual: True Flag curses Description: Use Curses to get the screen width Default: False manual: True -- This flag determines whether to show Git hashes in version strings -- Defaults to True because Hackage is a source release Flag release Description: This is an official release Default: True manual: True Flag freestanding Description: Build an Idris that doesn't use cabal Default: False manual: True Flag CI Description: Built everything using "-Werror", meant for CI-builds only Default: False manual: True Flag execonly Description: Build executables only, skip the libraries and RTS Default: False manual: True Library hs-source-dirs: src Exposed-modules: Idris.Core.Binary , Idris.Core.CaseTree , Idris.Core.Constraints , Idris.Core.DeepSeq , Idris.Core.Elaborate , Idris.Core.Evaluate , Idris.Core.Execute , Idris.Core.ProofState , Idris.Core.ProofTerm , Idris.Core.TT , Idris.Core.Typecheck , Idris.Core.Unify , Idris.Core.WHNF , Idris.Elab.Utils , Idris.Elab.Type , Idris.Elab.AsPat , Idris.Elab.Clause , Idris.Elab.Data , Idris.Elab.Record , Idris.Elab.Class , Idris.Elab.Instance , Idris.Elab.Provider , Idris.Elab.RunElab , Idris.Elab.Transform , Idris.Elab.Value , Idris.Elab.Term , Idris.REPL.Browse , Idris.AbsSyntax , Idris.AbsSyntaxTree , Idris.Apropos , Idris.ASTUtils , Idris.CaseSplit , Idris.Chaser , Idris.Colours , Idris.Completion , Idris.Coverage , Idris.DSL , Idris.DataOpts , Idris.DeepSeq , Idris.Delaborate , Idris.Directives , Idris.Docs , Idris.Docstrings , Idris.ElabDecls , Idris.ElabQuasiquote , Idris.Erasure , Idris.Error , Idris.ErrReverse , Idris.Help , Idris.IBC , Idris.IdeMode , Idris.IdrisDoc , Idris.Imports , Idris.Inliner , Idris.Interactive , Idris.Output , Idris.Parser , Idris.ParseHelpers , Idris.ParseOps , Idris.ParseExpr , Idris.ParseData , Idris.PartialEval , Idris.Primitives , Idris.ProofSearch , Idris.Prover , Idris.Providers , Idris.Reflection , Idris.REPL , Idris.REPLParser , Idris.Transforms , Idris.TypeSearch , Idris.Unlit , Idris.WhoCalls , Idris.CmdOptions , IRTS.BCImp , IRTS.Bytecode , IRTS.CodegenC , IRTS.CodegenCommon , IRTS.CodegenJavaScript , IRTS.Exports , IRTS.JavaScript.AST , IRTS.Compiler , IRTS.Defunctionalise , IRTS.DumpBC , IRTS.Inliner , IRTS.Lang , IRTS.LangOpts , IRTS.Simplified , IRTS.System , Pkg.Package , Util.DynamicLinker , Util.ScreenSize , Util.System Other-modules: Util.Pretty , Util.Net , Pkg.PParser -- Auto Generated , Paths_idris , Version_idris , Tools_idris Build-depends: base >=4 && <5 , annotated-wl-pprint >= 0.7 && < 0.8 , ansi-terminal < 0.7 , ansi-wl-pprint < 0.7 , 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 , 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 , 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 , unordered-containers < 0.3 , utf8-string < 1.1 , vector < 0.12 , vector-binary-instances < 0.3 , zip-archive > 0.2.3.5 && < 0.2.4 , zlib < 0.6 , safe Extensions: MultiParamTypeClasses , DeriveFoldable , DeriveTraversable , FunctionalDependencies , FlexibleContexts , FlexibleInstances , TemplateHaskell ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts if os(linux) cpp-options: -DLINUX build-depends: unix < 2.8 if os(freebsd) cpp-options: -DFREEBSD build-depends: unix < 2.8 -- if os(dragonfly) -- cpp-options: -DDRAGONFLY -- build-depends: unix < 2.8 if os(darwin) cpp-options: -DMACOSX build-depends: unix < 2.8 if os(windows) cpp-options: -DWINDOWS build-depends: Win32 < 2.4 if flag(FFI) build-depends: libffi < 0.2 cpp-options: -DIDRIS_FFI if flag(GMP) build-depends: libffi < 0.2 extra-libraries: gmp cpp-options: -DIDRIS_GMP if flag(curses) build-depends: hscurses < 1.5 cpp-options: -DCURSES if flag(freestanding) other-modules: Target_idris cpp-options: -DFREESTANDING if flag(CI) ghc-options: -Werror Executable idris Main-is: Main.hs hs-source-dirs: main Build-depends: idris , base , filepath , directory , haskeline >= 0.7 , transformers ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -funbox-strict-fields Executable idris-codegen-c Main-is: Main.hs hs-source-dirs: codegen/idris-codegen-c Build-depends: idris , base , filepath , haskeline >= 0.7 , transformers ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -funbox-strict-fields Executable idris-codegen-javascript Main-is: Main.hs hs-source-dirs: codegen/idris-codegen-javascript Build-depends: idris , base , filepath , haskeline >= 0.7 , transformers ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -funbox-strict-fields Executable idris-codegen-node Main-is: Main.hs hs-source-dirs: codegen/idris-codegen-node Build-depends: idris , base , filepath , haskeline >= 0.7 , transformers ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -funbox-strict-fields