search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
755 stars 70 forks source link

Moving closed notations at level 0 in anticipation of the removal of the Coq fallback ignoring levels when nothing else applies. #134

Closed herbelin closed 1 year ago

herbelin commented 1 year ago

Hi, as indicated in the title, this PR is in anticipation of a change of Coq's parsing rules (see e.g. coq/coq#17876 for details). For instance, Δ( c ), formerly at level 90, was used on the right of↓, which was expecting a notation at level less than 90. As another example, ⟨πD,πC⟩, formerly at level 100, was used as argument of ◯, as if it were at level less than 40.

So, the PR moves to level 0 the notations that have terminals on both sides (in general, there is little to gain not to do so, the only problem being if the starting symbol is also ending another notation).

There is another small change, requiring extra parentheses in the argument of the prefix notations `1 and `2.

If you agree with the change, this can be merged without delays.

jwiegley commented 1 year ago

This looks good to me, I will merge once CI passes.