git.iko.soy/Idris-dev
on 348cf91 help sign in
Idris-dev/src/Idris
21 files
../ AbsSyntax.hsmake TT aware of Set -> Type AbsSyntaxTree.hsAbstract matched terms from goal type in with clauses (like 'magic with' in Agda) 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.hsmake TT aware of Set -> Type Error.hsAllow inference of Sets at REPL IBC.hsPrimitive types for groups of 8, 16, 32, and 64 bits, and basic arithmetic and mutual conversion operations on them Imports.hsAdding support for Windows MingW32 Parser.hsPrimitive types for groups of 8, 16, 32, and 64 bits, and basic arithmetic and mutual conversion operations on them Primitives.hsString primitives 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