../ AbsSyntax.hsAllow 'rewrite ... in' to assert the resulting type "rewrite f ==> t in x" means that after applying the rewrite f, the required type of x must be t. This is primarily for readability of proofs built by successive rewritings.13 years ago AbsSyntaxTree.hsAllow 'rewrite ... in' to assert the resulting type "rewrite f ==> t in x" means that after applying the rewrite f, the required type of x must be t. This is primarily for readability of proofs built by successive rewritings.13 years ago Compiler.hsmake TT aware of Set -> Type14 years ago 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.13 years ago 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.13 years ago 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.15 years ago DataOpts.hsRemove the unused arg from lookup functions14 years ago Delaborate.hsImprove the "...is not solved" internal error to display something useful Fixes #361 Fixes #32113 years ago Docs.hsRemove the unused arg from lookup functions14 years ago ElabDecls.hsBeginnings of integer SIMD support (no backend yet)13 years ago ElabTerm.hsMerge pull request #383 from JanBessai/ITChar13 years ago Error.hsMake the type of ierror more general13 years ago Help.hsadd command to change current directory14 years ago IBC.hsMerge pull request #383 from JanBessai/ITChar13 years ago IdeSlave.hscleanups, rename List to SexpList to disambiguate13 years ago Imports.hsAdding support for Windows MingW3214 years ago Parser.hsMerge pull request #383 from JanBessai/ITChar13 years ago Primitives.hsMake ChType a member of IntTy ITChar.13 years ago 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 trace13 years ago Providers.hsRemove unused import13 years ago REPL.hsOptimization level selection13 years ago REPLParser.hssquash potential space leaks by using strict foldl14 years ago Transforms.hsuppercase modulenames14 years ago Unlit.hsFix Unlit to cope with documentation comment syntax14 years ago UnusedArgs.hsRemove the unused arg from lookup functions14 years ago