Hi! I'm having some issues understanding some caveats of notation levels in coq, and why certain terms are parsed a certain way.

I'm working with a lot of notation, and these are specifically the ones I'm having issues with (with some type information if that helps):

```
Notation "A ⟷ B" := (Compose A B)
(left associativity, at level 40)
Notation "'Z'" := Z_Spider (no associativity, at level 1)
Reserved Notation "⊙ zx" (at level 0). (* level 0 has right associativity *)
Fixpoint color_swap {nIn nOut} (zx : ZX nIn nOut) : ZX nIn nOut :=
...
where "⊙ zx" := (color_swap zx).
Inductive ZX : nat -> nat -> Type :=
| ...
| Z_Spider n m (α : R) : ZX n m
| Cup : ZX 2 0
| Cap : ZX 0 2
| Compose {n m o} (zx0 : ZX n m) (zx1 : ZX m o) : ZX n o.
| ...
```

Specifically I'm confused about why ⊙ is acting the following way:

```
Check ⊙ Z 0 0 0 ⟷ Z 0 0 0.
>>> ⊙ (Z 0 0 0 ⟷ Z 0 0 0) : ZX 0 0
Check ⊙ Cap ⟷ Cup.
>>> ⊙ (Cap) ⟷ Cup: ZX 0 0
```

Specifically, I'm unsure why `⊙ Z 0 0 0 ⟷ Z 0 0 0`

is applying `⊙`

to `(Z 0 0 0 ⟷ Z 0 0 0)`

and not just the first `Z 0 0 0`

(like i believe it should be `⊙ (Z 0 0 0) ⟷ Z 0 0 0`

or `(⊙ Z 0 0 0) ⟷ Z 0 0 0`

). From what I understand, `⊙`

is at level 0 and hence should bind the tightest, while `⟷`

should be the "outermost" function. The binding with the second check is what makes more sense to me.

If I expand the notation `Z`

to then try `⊙ Z_Spider 2 2 2 ⟷ Z_Spider 2 2 2`

, this doesn't actually parse.

I believe the discrepancy is probably because `Z`

itself is notation, but I don't really understand why?

you should specify the level for zx as well, that's what matters for parsing the "content" of your operator. Example:

Reserved Notation "⊢ Q" (at level 20, Q at level 200).

Your current notation has a level for zx, but that's decided via undocumented heuristics

Roughly, the semantics of my example is to add a production to "constr_20" that invokes "constr_200" to parse Q.

(sorry for the formatting but I'm screen-typing from an iPad)

I see, that actually makes a lot of sense

thank you so much!

Last updated: Jun 20 2024 at 12:02 UTC