Stream: Coq users

Topic: How to have multiple where statements for a single inductive

walker (Jun 21 2023 at 09:17):

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)

Gaëtan Gilbert (Jun 21 2023 at 09:26):

``````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`)

Gaëtan Gilbert (Jun 21 2023 at 09:27):

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

walker (Jun 21 2023 at 09:33):

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

Last updated: Jun 22 2024 at 16:02 UTC