Stream: Coq users

Topic: Notations with default precedence


view this post on Zulip Julin S (May 03 2022 at 10:54):

I was reading about precedence levels in notations.

There it's mentioned that:

the precedence level is mandatory (except for special cases whose level is canonical)

What are the special cases with canonical levels?

Just curious.

view this post on Zulip Julin S (May 03 2022 at 11:13):

Found this example where start and end symbols are terminals:

Notation "( x , y )" := (@pair _ _ x y).

Default notation level is 0.

Manual says notation level of the sub-expression itself is 200. Does that mean the x, y part of the @par _ _ x y part?


Last updated: Jan 29 2023 at 01:02 UTC