on db5973b help sign in
11 files
../ CaseTree.hsStrip impossible cases when building case trees 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.hsImproved type-directed name disambiguation Evaluate.hsevTree does not handle ImpossibleCase ProofShell.hsDisentangle Haskeline from the internals Idris ProofState.hsUnification fix ShellParser.hsFiddle with elaborator; update interp sample and test TT.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. Typecheck.hsMerge branch 'bitstring' of https://github.com/bitlisp/Idris-dev into bitlisp-bitstring Unify.hsUnification fix