git.iko.soy/Idris-dev
on c4e7ba2 help sign in
Idris-dev/src/Core
11 files
../ CaseTree.hsImprove evaluation of projection By caching result of evaluation, so that it's already evaluated when next projection happens. Constraints.hsMore platform agnostic now CoreParser.hsImprove evaluation of projection By caching result of evaluation, so that it's already evaluated when next projection happens. Elaborate.hsLimited type inference of types in where clauses Type signatures can now be omitted *only* if the type of the function can be determined completely from the first call. Evaluate.hsImprove evaluation of projection By caching result of evaluation, so that it's already evaluated when next projection happens. ProofShell.hsA small cleanup after missing some stray ends in the diff. ProofState.hsFix argument names in generated types for where blocks ShellParser.hsFiddle with elaborator; update interp sample and test TT.hsAdded postulate declarations postulate foo : type -- 'type' must return something of a collapsible type, i.e. a type with at most one instancei determined entirely by the indices, to ensure that it is unused at run-time. Typecheck.hsBetter dealing with name shadowing while building instances ...and while type checking completed terms Unify.hsBetter dealing with name shadowing while building instances ...and while type checking completed terms