on ddba413 help sign in
Idris-dev/src/Idris
12 files
../ AbsSyntax.hsAdd :a comment, to add most recent proof script to source file Compiler.hsAdded 'module' keyword to declare default namespace. 'main' must be in namespace 'main' Delaborate.hsNamespaces ElabDecls.hsNamespaces ElabTerm.hsNamespaces Error.hs:r and :e at the REPL. Imports.hsAdded log/exp (and lib/link directives) Parser.hsHierarchical namespaces; reorganised prelude accordingly Primitives.hsSeparate elaboration of declarations and terms Prover.hsAdd :a comment, to add most recent proof script to source file REPL.hsHierarchical namespaces; reorganised prelude accordingly REPLParser.hsAdd :a comment, to add most recent proof script to source file