../ CaseTree.hsAllow simple function types to be reflected13 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.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 Evaluate.hsBasic colourisation in REPL13 years ago Execute.hsSeparate IO and PrimIO PrimIO is the internal primitive, IO is the user version which requires an explicit World token to be passed in which programmers have no access to directly. Fixes #185 and fixes #32513 years ago ProofShell.hsRemove the unused arg from lookup functions14 years ago ProofState.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 ShellParser.hsFiddle with elaborator; update interp sample and test15 years ago TT.hsChange treatment of underscore in lambda Treat as unnamed variables, rather than as patterns13 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.hsBetter unification errors when name is out of scope In particular, a unification problem which cannot be solved because it uses a variable not in scope where the metavariable is bound. Fixes #34213 years ago