Name: idris Version: 0.9.6.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.6 Build-type: Custom Data-files: rts/libidris_rts.a 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/System/Concurrency/*.idr lib/Data/*.idr lib/Debug/*.idr tutorial/examples/*.idr lib/base.ipkg config.mk rts/*.c rts/*.h rts/Makefile js/*.js source-repository head type: git location: git://github.com/edwinb/Idris-dev.git Executable idris Main-is: Main.hs hs-source-dirs: src Other-modules: Core.TT, Core.Evaluate, 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.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, Util.Pretty, Util.System, Pkg.Package, Pkg.PParser, IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified, IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Inliner, IRTS.Compiler, IRTS.CodegenJava, 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, pretty Extensions: MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, TemplateHaskell ghc-prof-options: -auto-all -caf-all ghc-options: -rtsopts