categories
categories copied to clipboard
Fails to compile with idris 1.3.1
$ idris --install categories.ipkg Entering directory `./src' Type checking ./Relation.idr Type checking ./Setoid.idr Type checking ./Operation.idr Type checking ./Algebra.idr Type checking ./Algebra/Hierarchy.idr Type checking ./Relation/Hierarchy.idr Type checking ./Setoid/Natural.idr Type checking ./Setoid/BuiltIn.idr Type checking ./Setoid/Arrow.idr Type checking ./Setoid/SetoidFunction.idr ./Setoid/SetoidFunction.idr:9:1-14:80: | 9 | record SetoidFunction (A: Setoid) (B: Setoid) where | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ... When checking left hand side of SetoidFunction.SetoidFunction.param_A: When checking argument A to SetoidFunction.MkSetoidFunction: A is not a valid name for a pattern variable
Hi. It should have been fixed by #5, I merged it, please check again