Closed MatthiasHu closed 1 year ago
Are there any advantages of syntax
declarations that I might be missing? (Let me ping @mzeuner just because you wrote the ones for ∘a
and ∘r
:-) )
For the slim chance that there is such an advantage, we can still revert -> merging.
This PR replaces
syntax
declarations whichby ordinary infix (or mixfix) operator declarations.
The motivation for avoiding syntax declarations is that Agdas behavior around them can be confusing, for example:
_⇒_
(fromNaturalTransformation.Base
), in a hole and ask for its type (or try to "refine", or "give" the hole), you get a "Not in scope" error. (If I understand correctly,_⇒_
does indeed not exist as a name. But it is easy to expect it to exist.)open ... using (...)
, you have to write the name it refers to, even though you then never use that name.