categories icon indicating copy to clipboard operation
categories copied to clipboard

Fails to compile with idris 1.3.1

Open tj800x opened this issue 6 years ago • 1 comments

$ 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

tj800x avatar Oct 23 '18 23:10 tj800x

Hi. It should have been fixed by #5, I merged it, please check again

danilkolikov avatar Oct 24 '18 08:10 danilkolikov