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 ?

Paolo Giarrusso (Jun 21 2023 at 09:23):

(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: Oct 13 2024 at 01:02 UTC