on 0338d39 help sign in
Idris-dev/src/Idris
18 files
../ AbsSyntax.hsWork towards making {static} arguments and specialisation work properly Compiler.hsBetter name-chasing in Compiler Coverage.hsMore on errors; propagate line numbers DSL.hsGive up type class resolution sooner 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.hsMore on errors; propagate line numbers ElabDecls.hsFix case statements in type signatures ElabTerm.hsWork towards making {static} arguments and specialisation work properly Error.hsCheck definitions structurally as well as by name in conversion IBC.hsBetter type class resolution Imports.hsAdded support for literate programming with bird tracks (use .lidr extension) Parser.hsTry to get line numbers better Primitives.hsSet totality of primitive operators Prover.hsAdded 'abandon' command in proof mode (Alternatively, :q) REPL.hsWork towards making {static} arguments and specialisation work properly REPLParser.hsAdd :total command 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.