Name: idris Version: 0.9.10 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: jsrts/Runtime-browser.js jsrts/Runtime-common.js jsrts/Runtime-node.js jsrts/jsbn/jsbn.js jsrts/jsbn/LICENSE rts/idris_gc.h rts/idris_gmp.h rts/idris_main.c rts/idris_rts.h rts/idris_stdfgn.h rts/libtest.c Extra-source-files: Makefile config.mk rts/*.c rts/*.h rts/Makefile libs/Makefile libs/prelude/prelude.ipkg libs/prelude/Prelude/*.idr libs/prelude/Decidable/*.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/Decidable/*.idr libs/base/Language/*.idr libs/base/Language/Reflection/*.idr libs/base/Makefile libs/base/Network/*.idr libs/base/System/Concurrency/*.idr libs/effects/Makefile libs/effects/effects.ipkg libs/effects/Effect/*.idr libs/effects/*.idr libs/javascript/*.idr libs/javascript/JavaScript/*.idr libs/javascript/Makefile libs/javascript/javascript.ipkg llvm/*.c llvm/Makefile tutorial/examples/*.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/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/reg021/run test/reg021/*.idr test/reg021/expected test/reg022/run test/reg022/*.idr test/reg022/expected test/reg023/run test/reg023/*.idr test/reg023/expected test/reg024/run test/reg024/*.idr test/reg024/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 test/test029/run test/test029/*.idr test/test029/expected test/test030/run test/test030/*.idr test/test030/expected test/test031/run test/test031/*.idr test/test031/expected test/test032/run test/test032/*.idr test/test032/input test/test032/expected test/test033/run test/test033/*.idr test/test033/expected test/test034/run test/test034/expected source-repository head type: git location: git://github.com/idris-lang/Idris-dev.git Flag LLVM Description: Build the LLVM backend Default: False manual: True Flag FFI Description: Build support for libffi Default: False manual: True Flag GMP Description: Use GMP for Integers Default: False manual: True Executable idris Main-is: Main.hs hs-source-dirs: src Other-modules: Core.CaseTree , Core.Constraints , Core.Elaborate , Core.Evaluate , Core.Execute , Core.ProofState , Core.TT , Core.Typecheck , Core.Unify , Idris.AbsSyntax , Idris.AbsSyntaxTree , Idris.CaseSplit , Idris.Chaser , Idris.Colours , Idris.Completion , Idris.Coverage , Idris.DSL , Idris.DataOpts , Idris.DeepSeq , Idris.Delaborate , Idris.Docs , Idris.ElabDecls , Idris.ElabTerm , Idris.Error , Idris.Help , Idris.IBC , Idris.IdeSlave , Idris.Imports , Idris.Inliner , Idris.Parser , Idris.ParseHelpers , Idris.ParseOps , Idris.ParseExpr , Idris.ParseData , Idris.PartialEval , Idris.Primitives , Idris.ProofSearch , Idris.Prover , Idris.Providers , Idris.REPL , Idris.REPLParser , Idris.Transforms , Idris.Unlit , Idris.UnusedArgs , IRTS.BCImp , IRTS.Bytecode , IRTS.CodegenC , IRTS.CodegenCommon , IRTS.CodegenJava , IRTS.CodegenJavaScript , IRTS.Compiler , IRTS.Defunctionalise , IRTS.DumpBC , IRTS.Inliner , IRTS.Java.ASTBuilding , IRTS.Java.JTypes , IRTS.Java.Mangling , IRTS.Java.Pom , IRTS.Lang , IRTS.Simplified , Util.Pretty , Util.System , Util.DynamicLinker , Util.Net , Pkg.Package , Pkg.PParser -- Auto Generated Paths_idris Build-depends: base >=4 && <5 , Cabal , ansi-terminal , ansi-wl-pprint , binary , bytestring , containers , directory , directory >= 1.2 , filepath , haskeline >= 0.7 , language-java >= 0.2.6 , mtl --, parsec >= 3 , parsers == 0.9 , pretty , process , split , text , time >= 1.4 , transformers , trifecta == 1.1 , unordered-containers , utf8-string , vector , vector-binary-instances , network , xml , deepseq Extensions: MultiParamTypeClasses , FunctionalDependencies , FlexibleInstances , TemplateHaskell ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts if os(linux) cpp-options: -DLINUX build-depends: unix if os(freebsd) cpp-options: -DFREEBSD 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.8.* , llvm-general-pure == 3.3.8.* else other-modules: Util.LLVMStubs if flag(FFI) build-depends: libffi cpp-options: -DIDRIS_FFI if flag(GMP) build-depends: libffi cpp-options: -DIDRIS_GMP