../ CaseTree.hsDon't inline for compilation (because the evaluator makes bad choices) Instead, inline the compile-time representation to help the totality checker only. This can cause subexpressions to be duplicated, so should be avoided at run-time. For the run-time rep…13 years ago Constraints.hsDocumentation comment additions14 years ago CoreParser.hsParse empty comments13 years ago Elaborate.hsGive Pi bindings the proper name when elaborating lambdas Fixes #36013 years ago Evaluate.hsDon't inline for compilation (because the evaluator makes bad choices) Instead, inline the compile-time representation to help the totality checker only. This can cause subexpressions to be duplicated, so should be avoided at run-time. For the run-time rep…13 years ago Execute.hsSpecial-case prim__believe_me13 years ago ProofShell.hsRemove the unused arg from lookup functions14 years ago ProofState.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 ShellParser.hsFiddle with elaborator; update interp sample and test15 years ago TT.hsFix term size calculation for inlining Now counting binders other than Let, so lots of things previously inlined over-aggressively are now not inlined.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.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