I want to define multiple Notatons for the same Inductive type

Basically I want to:

```
Reserved Notation "Σ '⊢' x '⇒' y" (at level 20, x at next level, y at next level).
Reserved Notation "Σ '⊢' x '[⇒]' y" (at level 20, x at next level, y at next level).
Inductive FOO: nat -> nat -> nat -> Prop :=
where "Σ '⊢' t1 '⇒' t2" := (FOO Σ t1 t2)
where "Σ '⊢' x '[⇒]' y":= (forall ts, PIn ts (zip x y) -> Σ ⊢ fst ts ⇒ snd ts).
```

The point is in the real `FOO`

, it uses `Σ '⊢' x '[⇒]' y`

alot and I prefer to use the notation instead of the expansion (and most certainly I don't want to put it in a definitin of its own. It also helps with detecting bugs quickly visually.

My question is there away to make coq accept this kind of notations ?

(deleted)

```
Reserved Notation "Σ '⊢' x '⇒' y" (at level 20, x at next level, y at next level).
Reserved Notation "Σ '⊢' x '[⇒]' y" (at level 20, x at next level, y at next level).
Inductive FOO: nat -> nat -> nat -> Prop :=
where "Σ '⊢' t1 '⇒' t2" := (FOO Σ t1 t2)
and "Σ '⊢' x '[⇒]' y":= (forall ts, PIn ts (zip x y) -> Σ ⊢ fst ts ⇒ snd ts).
```

(`and`

instead of the second `where`

)

I don't know if it's possible to use the first notation in the definition of the second though

yes you can! and it worked, thanks a lot!

Last updated: Jun 22 2024 at 16:02 UTC