Stream: Coq users

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


view this post on Zulip 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 ?

view this post on Zulip Paolo Giarrusso (Jun 21 2023 at 09:23):

(deleted)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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