git.iko.soy/Idris-dev
on 3c0f4dc help sign in
Idris-dev/src/Idris
25 files
../ AbsSyntax.hsMerge pull request #362 from david-christiansen/cmdline-exec AbsSyntaxTree.hsSkeleton of stub-generating LLVM codegen 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.hsBeginnings of integer SIMD support (no backend yet) ElabTerm.hsBeginnings of integer SIMD support (no backend yet) Error.hsMake the type of ierror more general Help.hsadd command to change current directory IBC.hsBeginnings of integer SIMD support (no backend yet) IdeSlave.hscleanups, rename List to SexpList to disambiguate Imports.hsAdding support for Windows MingW32 Parser.hsBeginnings of integer SIMD support (no backend yet) Primitives.hsBeginnings of integer SIMD support (no backend yet) 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.hsSkeleton of stub-generating LLVM codegen 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