../ CaseTree.hsTweak totality checker14 years ago Constraints.hsMore platform agnostic now14 years ago CoreParser.hsmake TT aware of Set -> Type14 years ago Elaborate.hsmake TT aware of Set -> Type14 years ago Evaluate.hsA couple of small improvements to termination checking * inlining to help out * %assert_total doesn't allow inlining so as not to break totality for functions which rely on the asserted function * bug fix for mutual recursion - build size graphs before d…14 years ago ProofShell.hsmake TT aware of Set -> Type14 years ago ProofState.hsmake TT aware of Set -> Type14 years ago ShellParser.hsFiddle with elaborator; update interp sample and test15 years ago TT.hsAbstract matched terms from goal type in with clauses (like 'magic with' in Agda)14 years ago Typecheck.hsmake TT aware of Set -> Type14 years ago Unify.hsBetter dealing with name shadowing while building instances ...and while type checking completed terms14 years ago