6Maintainer: Edwin Brady <eb@cs.st-andrews.ac.uk>
7Homepage: http://www.idris-lang.org/
10Category: Compilers/Interpreters, Dependent Types
11Synopsis: Functional Programming Language with Dependent Types
12Description: Idris is a general purpose language with full dependent types.
13 It is compiled, with eager evaluation.
14 Dependent types allow types to be predicated on values,
15 meaning that some aspects of a program's behaviour can be
16 specified precisely in the type. The language is closely
17 related to Epigram and Agda. There is a tutorial at <http://www.idris-lang.org/documentation>.
20 * Full dependent types with dependent pattern matching
22 * where clauses, with rule, simple case expressions,
23 pattern matching let and lambda bindings
25 * Type classes, monad comprehensions
27 * do notation, idiom brackets, syntactic conveniences for lists,
28 tuples, dependent pairs
34 * Indentation significant syntax, extensible syntax
36 * Tactic based theorem proving (influenced by Coq)
38 * Cumulative universes
40 * Simple foreign function interface (to C)
42 * Hugs style interactive environment
47Data-files: rts/libidris_rts.a rts/idris_rts.h rts/idris_gc.h
48 rts/idris_stdfgn.h rts/idris_main.c rts/idris_gmp.h
50Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr
51 lib/Network/*.idr lib/Control/*.idr
52 lib/Control/Monad/*.idr lib/Language/*.idr
53 lib/System/Concurrency/*.idr
55 tutorial/examples/*.idr lib/base.ipkg
57 rts/*.c rts/*.h rts/Makefile
61 location: git://github.com/edwinb/Idris-dev.git
67 Other-modules: Core.TT, Core.Evaluate, Core.Typecheck,
68 Core.ProofShell, Core.ProofState, Core.CoreParser,
69 Core.ShellParser, Core.Unify, Core.Elaborate,
70 Core.CaseTree, Core.Constraints,
72 Idris.AbsSyntax, Idris.AbsSyntaxTree,
73 Idris.Parser, Idris.REPL,
74 Idris.REPLParser, Idris.ElabDecls, Idris.Error,
75 Idris.Delaborate, Idris.Primitives, Idris.Imports,
76 Idris.Compiler, Idris.Prover, Idris.ElabTerm,
77 Idris.Coverage, Idris.IBC, Idris.Unlit,
78 Idris.DataOpts, Idris.Transforms, Idris.DSL,
79 Idris.UnusedArgs, Idris.Docs,
81 Util.Pretty, Util.System,
82 Pkg.Package, Pkg.PParser,
84 IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,
85 IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Inliner,
86 IRTS.Compiler, IRTS.CodegenJava, IRTS.BCImp,
91 Build-depends: base>=4 && <5, parsec, mtl, Cabal,
92 haskeline>=0.7, split,
93 containers, process, transformers, filepath,
94 directory, binary, bytestring, pretty
96 Extensions: MultiParamTypeClasses, FunctionalDependencies,
97 FlexibleInstances, TemplateHaskell
98 ghc-prof-options: -auto-all -caf-all
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list