git.iko.soy/Idris-dev
on 449e292 help sign in
Idris-dev/src/Idris
21 files
../ AbsSyntax.hsmake TT aware of Set -> Type AbsSyntaxTree.hsmake TT aware of Set -> Type Compiler.hsmake TT aware of Set -> Type Coverage.hsTweak totality checker 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.hsAdd collapsing optimisation and more aggressive erasure Delaborate.hsmake TT aware of Set -> Type Docs.hsbetter lookup for operators ElabDecls.hsA couple of small improvements to termination checking * inlining to help out * %assert_total doesn't allow inlining so as not to break totality for functions which rely on the asserted function * bug fix for mutual recursion - build size graphs before d… ElabTerm.hsmake TT aware of Set -> Type Error.hsAllow inference of Sets at REPL IBC.hsFix traversal of size change graphs Fixes issue #134 - new regression test added Imports.hsAdding support for Windows MingW32 Parser.hsA couple of small improvements to termination checking * inlining to help out * %assert_total doesn't allow inlining so as not to break totality for functions which rely on the asserted function * bug fix for mutual recursion - build size graphs before d… Primitives.hsmake TT aware of Set -> Type Prover.hsA couple of small improvements to termination checking * inlining to help out * %assert_total doesn't allow inlining so as not to break totality for functions which rely on the asserted function * bug fix for mutual recursion - build size graphs before d… REPL.hsAdded the ability to dump bytecode to a file REPLParser.hsAdding support for Windows MingW32 Transforms.hsuppercase modulenames Unlit.hsFix Unlit to cope with documentation comment syntax UnusedArgs.hsMerge branch 'master' of https://github.com/raichoo/Idris-dev