../ CaseTree.hsFix bug in compilation of optimised Nats13 years ago Constraints.hsDocumentation comment additions14 years ago CoreParser.hsAdded 'quoteGoal x by p in e' syntax meaning, let x = p [current goal] in e Additionally, the value of x is normalised, which means p can be a compile-time only %reflection function used to prove something interesting in e. See test030 for an example of au…13 years ago Elaborate.hsBetter representation and rendering of generated names13 years ago Evaluate.hsCompile Nat as Int, (and plus/mult/fromInteger)13 years ago Execute.hsAdd skeleton of inliner13 years ago ProofShell.hsRemove the unused arg from lookup functions14 years ago ProofState.hsUnification fix to avoid giving up on recoverable errors13 years ago ShellParser.hsFiddle with elaborator; update interp sample and test15 years ago TT.hsGenerate simpler names with showCG13 years ago Typecheck.hsSimplify evaluator It tries to support too much, but since it's part of the kernel it should do as little clever stuff as possible. Now just normalises, simplifies or specialises, the latter two simply meaning that certain names are blocked from being redu…13 years ago Unify.hsUnification fix to avoid giving up on recoverable errors13 years ago