on 047be9e help sign in
Idris-dev/src/Idris
18 files
../ AbsSyntax.hs-i option added (thanks to Dirk Ullrich) Compiler.hsAdd mkLazyForeign primitive 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.hsFix reverse elaboration of dependent pairs ElabDecls.hsDon't normalise types 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.hs-i option added (thanks to Dirk Ullrich) Imports.hsAdd --ibcsubdir option (thanks to Dirk Ullrich) Parser.hs-i option added (thanks to Dirk Ullrich) Primitives.hsAdded prim__bigIntToInt (needs latest EpiVM) Prover.hsCheck patterns are inaccessible REPL.hsPass pattern variable names to match compiler 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.