git.iko.soy/Idris-dev
on ff0fbfa help sign in
Idris-dev/test/reg012
3 files
../ expectedFix another unification problem (solving things which shouldn't be) reg012.lidrAdded 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. runMerge branch 'AddMissingStrLen' of https://github.com/JanBessai/Idris-dev into JanBessai-AddMissingStrLen