on e88a135 help sign in
Idris-dev/src/Idris
19 files
../ AbsSyntax.hsAdded simple library packaging system Now used for the prelude (see lib/base.ipkg) AbsSyntaxTree.hsAdded simple library packaging system Now used for the prelude (see lib/base.ipkg) Compiler.hsSet up for adding new compiler back ends more easily Coverage.hsPass pattern variable names to match compiler DSL.hsChange meaning of alternative syntax (| a , b , ... |) Now takes the first alternative to elaborate,rather than requiring exactly one to work. Old behaviour reserved for disambiguating namespaces. DataOpts.hsPass pattern variable names to match compiler Delaborate.hsSpeed improvements when code contains type errors Identify "unrecoverable" unification failures so that type checking doesn't continue to search all the alternative overloadings and orderings. ElabDecls.hsQuicker resolution of overloaded names By checking the name's type against the goal type rather than fully checking. ElabTerm.hsFix FLOATOP properly Error.hsNo need to qualify unambiguous names on :p IBC.hsAdded binding form to syntax rules (and updated tutorial accordingly) Imports.hsAdd --ibcsubdir option (thanks to Dirk Ullrich) Parser.hssatisfy hlint Primitives.hsAdded fork (but not working properly yet) Prover.hsadded proof list REPL.hsAdded simple library packaging system Now used for the prelude (see lib/base.ipkg) REPLParser.hsSet up for adding new compiler back ends more easily Transforms.hsTest file for new VM, hook up parser Unlit.hsRemoved need for terminating ; A declaration is now considered terminated on encountering a token in the same column as the declaration began - or on encountering a semicolon. Libraries and some tests updated.