git.iko.soy/Idris-dev
on decad94 help sign in
Idris-dev/test/reg005
3 files
../ expectedNormalise LHS before compilation ...otherwise in some situations the forcing optimisation may lead to uncompilable code reg005.idrChanged approach to unification Instead of failing immediately, maintain a list of blocked problems and refine during elaboration. runNormalise LHS before compilation ...otherwise in some situations the forcing optimisation may lead to uncompilable code