git.iko.soy/Idris-dev
on f8ea178 help sign in
Idris-dev/src/Idris
25 files
../ AbsSyntax.hsMerge pull request #362 from david-christiansen/cmdline-exec AbsSyntaxTree.hsMerge pull request #362 from david-christiansen/cmdline-exec Compiler.hsmake TT aware of Set -> Type Completion.hsAdded 'mrefine' tactic Like refine, but uses matching instead of unification to resolve implicit arguments. All will become clear, I hope :). This is intended for an additional style of pattern matching (on types) for better explanation of proofs. Coverage.hsNew size change graph builder Looks at patterns, rather than case tree, and therefore finds it easier to spot structurally smaller arguments which are more complex. 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.hsRemove the unused arg from lookup functions Delaborate.hsFix :t for metavariables Fixes issue #280 Docs.hsRemove the unused arg from lookup functions ElabDecls.hsMerge pull request #358 from david-christiansen/unite-the-primitives ElabTerm.hsAdded %unifyLog construct For debugging purposes %unifyLof t will give a trace of unification problems while elaborating t Also, log levels 6 and above will give the trace Error.hsMake the type of ierror more general Help.hsadd command to change current directory IBC.hsAdd scripts IdeSlave.hscleanups, rename List to SexpList to disambiguate Imports.hsAdding support for Windows MingW32 Parser.hsAdded %unifyLog construct For debugging purposes %unifyLof t will give a trace of unification problems while elaborating t Also, log levels 6 and above will give the trace Primitives.hsSpecial-case prim__believe_me Prover.hsAdded %unifyLog construct For debugging purposes %unifyLof t will give a trace of unification problems while elaborating t Also, log levels 6 and above will give the trace Providers.hsRemove unused import REPL.hsAdd scripts REPLParser.hssquash potential space leaks by using strict foldl Transforms.hsuppercase modulenames Unlit.hsFix Unlit to cope with documentation comment syntax UnusedArgs.hsRemove the unused arg from lookup functions