../ CaseTree.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 Constraints.hsDocumentation comment additions14 years ago CoreParser.hsParse empty comments13 years ago Elaborate.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 Evaluate.hsFix Haddock parser error13 years ago Execute.hsExtract getOp to top level defn13 years ago ProofShell.hsRemove the unused arg from lookup functions14 years ago ProofState.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 ShellParser.hsFiddle with elaborator; update interp sample and test15 years ago TT.hsImplement 'pretty' for B{8,16,32,64}13 years ago Typecheck.hsCheck that explicitly given implicit args unify with inferred versions Also exposed a unification bug which unified things which shouldn't be: f x = f y does not imply x = y unless f is injective, and this was not properly checked.13 years ago Unify.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