../ AbsSyntax.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 AbsSyntaxTree.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 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.hsFix :t for metavariables Fixes issue #28014 years ago Docs.hsRemove the unused arg from lookup functions14 years ago ElabDecls.hsEXPERIMENTAL: Syntax for applying functions by expected type "t <== f" applies a function f to arguments in such a way that it returns something of type t. The <== is a placeholder syntax until someone comes up with something better. (Alternative: t by f, …13 years ago 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 trace13 years ago Error.hsMake the type of ierror more general13 years ago Help.hsadd command to change current directory14 years ago IBC.hsAdded backend target specification to %lib, %link and %include directives13 years ago IdeSlave.hscleanups, rename List to SexpList to disambiguate13 years ago Imports.hsAdding support for Windows MingW3214 years ago 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 trace13 years ago Primitives.hsAdd type annotations to Primitives.hs to aid in understanding13 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.hsClean up implementation of type providers13 years ago REPL.hsTake care with 'let' in specialiser - avoid duplicating a redex Let now only reduces if the binding appears at most once in scope during specialisation13 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