-
Notifications
You must be signed in to change notification settings - Fork 58
Open
Description
I'm seeing some weird behavior with the current HoTT-Agda library in Agda 2.5.1.1: frequently when I want to compose two complicated paths, Agda is unwilling to parse the path-composition operator infix. It says complains something like
Don't know how to parse
(blah1)
∙ (blah2)
Could mean any one of
((blah1)
∙)
(blah2)
_∙_
(blah1)
(blah2)
Operators used in the grammar:
∙ (infixr operator, level 80) [_∙_ (/home/shulman/hott/agda/core/lib/PathGroupoid.agda:18,3-6)]
(the treatment of operators was changed in Agda 2.5.1, so code that
used to parse may have to be changed)Here (blah1) and (blah2) are simple function applications, not mixfix operations, and both enclosed in parentheses, so I don't see what the ambiguity could possibly be. I haven't managed to isolate a MWE, but I wonder whether anyone else is seeing this? Is there an easy solution?
Metadata
Metadata
Assignees
Labels
No labels