git.iko.soy/Idris-dev
on 04d6f00 help sign in
Idris-dev/src/Idris
21 files
../ AbsSyntax.hsmake TT aware of Set -> Type AbsSyntaxTree.hsA small amount of proof automation, via tactic reflection Compiler.hsmake TT aware of Set -> Type Coverage.hsCorrect totality check of f=f, and add regression test 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 sure names are not defined more than once Fixes issue #124 Docs.hsbetter lookup for operators ElabDecls.hsMake sure names are not defined more than once Fixes issue #124 ElabTerm.hsA small amount of proof automation, via tactic reflection Error.hsAllow inference of Sets at REPL IBC.hsA small amount of proof automation, via tactic reflection Imports.hsAdding support for Windows MingW32 Parser.hsA small amount of proof automation, via tactic reflection 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