on cbc8a13 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.idrMake 'Type' the type of types instead of Sets ...after mailing list discussion runNormalise LHS before compilation ...otherwise in some situations the forcing optimisation may lead to uncompilable code