git.iko.soy/Idris-dev
on 96031d1 help sign in
Idris-dev/src/Idris
18 files
../ AbsSyntax.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. Compiler.hsInstall support headers; allow arbitrary types in foreign calls Coverage.hsRemove some unused code 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.hsCoverage checker Not quite complete - a bug (which I know how to fix) makes some things appear not covering even though they are. Results currently used only for pruning case trees in compiled code. There is a small performance penalty - coverage checking … Delaborate.hsFix bug with de-elaboration of sigma types ElabDecls.hsNormalise types before applying forcing ElabTerm.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. Error.hsCheck definitions structurally as well as by name in conversion IBC.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. Imports.hsAdd --ibcsubdir option (thanks to Dirk Ullrich) Parser.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. Primitives.hsAdded prim__bigIntToInt (needs latest EpiVM) Prover.hsSome playing around with widths to make everything look nicer. REPL.hsAn introduction REPLParser.hsQuick hack at :info for exploring type classes Transforms.hsAdd Transform module; make implicit args lazy 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.