git.iko.soy/Idris-dev
on 59456cd help sign in
Idris-dev/src/Core
12 files
../ CaseTree.hsBasically working executor/interpreter Constraints.hsDocumentation comment additions CoreParser.hsAdded rewrite ... in ... construct rewrite prf in v rewrites the goal type using prf. It is equivalent to applying replace, without the need to provide a predicate. It works by applying the rewrite tactic with prf before elaborating v. Elaborate.hsIf the goal is not a function type when elaborating \, invent one ...and attempt to solve it by unification Evaluate.hsBasically working executor/interpreter Execute.hsImprove FFI accuracy in executor ProofShell.hsDisentangle Haskeline from the internals Idris ProofState.hsFix some INTERNAL ERRORs which aren't (non-function type, nothing to introduce) (And the crowd goes wild) ShellParser.hsFiddle with elaborator; update interp sample and test TT.hsDocumentation improvement Typecheck.hsFix some INTERNAL ERRORs which aren't (non-function type, nothing to introduce) (And the crowd goes wild) Unify.hsUnification fix