Name: idris Version: 0.9.9 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.6 Build-type: Custom Data-files: rts/idris_rts.h rts/idris_gc.h rts/idris_stdfgn.h rts/idris_main.c rts/idris_gmp.h rts/libtest.c js/Runtime-common.js js/Runtime-node.js js/Runtime-browser.js Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr lib/Network/*.idr lib/Control/*.idr lib/Control/Monad/*.idr lib/Language/*.idr lib/Language/Reflection/*.idr lib/System/Concurrency/*.idr lib/Data/*.idr lib/Debug/*.idr lib/Data/Vect/*.idr lib/Decidable/*.idr tutorial/examples/*.idr lib/base.ipkg effects/Makefile effects/*.idr effects/Effect/*.idr effects/effects.ipkg javascript/Makefile javascript/JavaScript/*.idr javascript/*.idr javascript/javascript.ipkg config.mk rts/*.c rts/*.h rts/Makefile llvm/*.c llvm/Makefile js/*.js java/*.xml Makefile 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/reg005/run test/reg005/*.idr test/reg005/expected test/reg006/run test/reg006/*.idr test/reg006/expected test/reg007/run test/reg007/*.lidr test/reg007/expected test/reg008/run test/reg008/*.idr test/reg008/expected test/reg009/run test/reg009/*.lidr test/reg009/expected test/reg010/run test/reg010/*.idr test/reg010/expected test/reg011/run test/reg011/*.idr test/reg011/expected test/reg012/run test/reg012/*.lidr test/reg012/expected test/reg013/run test/reg013/*.idr test/reg013/expected test/reg014/run test/reg014/*.idr test/reg014/expected test/reg015/run test/reg015/*.idr test/reg015/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/reg019/run test/reg019/*.idr test/reg019/expected test/reg020/run test/reg020/*.idr test/reg020/expected test/test001/run test/test001/*.idr test/test001/expected test/test002/run test/test002/*.idr test/test002/expected test/test003/run test/test003/*.lidr test/test003/expected test/test004/run test/test004/*.idr test/test004/expected test/test005/run test/test005/*.idr test/test005/expected test/test006/run test/test006/*.idr test/test006/expected test/test007/run test/test007/*.idr test/test007/expected test/test008/run test/test008/*.idr test/test008/expected test/test009/run test/test009/*.idr test/test009/expected test/test010/run test/test010/*.idr test/test010/expected test/test011/run test/test011/*.idr test/test011/expected test/test012/run test/test012/*.idr test/test012/expected test/test013/run test/test013/*.idr test/test013/expected test/test014/run test/test014/*.idr test/test014/test test/test014/expected test/test015/run test/test015/*.idr test/test015/expected test/test016/run test/test016/*.idr test/test016/expected test/test017/run test/test017/*.idr test/test017/expected test/test018/run test/test018/*.idr test/test018/expected test/test019/run test/test019/*.lidr test/test019/expected test/test020/run test/test020/*.idr test/test020/expected test/test021/run test/test021/*.idr test/test021/testFile test/test021/expected test/test022/run test/test022/*.idr test/test022/expected test/test023/run test/test023/*.idr test/test023/expected test/test024/run test/test024/*.idr test/test024/input test/test024/expected test/test025/run test/test025/*.idr test/test025/expected test/test026/run test/test026/*.idr test/test026/input test/test026/theType test/test026/theOtherType test/test026/expected test/test027/run test/test027/*.idr test/test027/expected test/test028/run test/test028/*.idr test/test028/expected source-repository head type: git location: git://github.com/edwinb/Idris-dev.git Flag NoEffects Description: Do not build the effects package Default: False Flag LLVM Description: Build the LLVM backend Default: True manual: True Executable idris Main-is: Main.hs hs-source-dirs: src Other-modules: Core.TT, Core.Evaluate, Core.Execute, Core.Typecheck, Core.ProofShell, Core.ProofState, Core.CoreParser, Core.ShellParser, Core.Unify, Core.Elaborate, Core.CaseTree, Core.Constraints, Idris.AbsSyntax, Idris.AbsSyntaxTree, Idris.Parser, Idris.Help, Idris.IdeSlave, Idris.REPL, Idris.REPLParser, Idris.ElabDecls, Idris.Error, Idris.Delaborate, Idris.Primitives, Idris.Imports, Idris.Compiler, Idris.Prover, Idris.ElabTerm, Idris.Coverage, Idris.IBC, Idris.Unlit, Idris.DataOpts, Idris.Transforms, Idris.DSL, Idris.UnusedArgs, Idris.Docs, Idris.Completion, Idris.PartialEval, Idris.Providers, Util.Pretty, Util.System, Util.DynamicLinker, Pkg.Package, Pkg.PParser, IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified, IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Inliner, IRTS.Compiler, IRTS.CodegenJava, IRTS.Java.ASTBuilding, IRTS.Java.JTypes, IRTS.Java.Mangling, IRTS.BCImp, IRTS.CodegenJavaScript, IRTS.CodegenCommon, IRTS.DumpBC Paths_idris Build-depends: base>=4 && <5, parsec>=3, mtl, Cabal, haskeline>=0.7, split, directory, containers, process, transformers, filepath, directory, binary, bytestring, text, pretty, language-java>=0.2.2, libffi, vector, vector-binary-instances Extensions: MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, TemplateHaskell ghc-prof-options: -auto-all -caf-all ghc-options: -rtsopts if os(linux) cpp-options: -DLINUX build-depends: unix if os(darwin) cpp-options: -DMACOSX build-depends: unix if os(windows) cpp-options: -DWINDOWS build-depends: Win32 if flag(LLVM) other-modules: IRTS.CodegenLLVM cpp-options: -DIDRIS_LLVM build-depends: llvm-general==3.3.5.* else other-modules: Util.LLVMStubs