Plusieurs clauses Where pour la notation réservée en Coq?

Question

J'ai un tas de types de données mutuellement inductifs déclarés en utilisant with, et je voudrais définir un Notation pour chacun d'entre eux que je peux utiliser pendant que je les définis.

Je suis au courant des clauses Reserved Notations et with, mais je ne peux pas comprendre la syntaxe pour définir des notations multiples qui sont disponibles pour tous mes types mutuellement inductifs.

Est-il possible de définir plusieurs clauses where dans Notations, et si oui, est-ce que quelqu'un a un exemple de ce que je peux voir?

Answer 1

Un exemple:

Reserved Notation "# n" (at level 80). 
Reserved Notation "! n" (at level 80). 

Inductive even : nat -> Set := 
    | ev0 : #0 
    | evS : forall n, !n -> # S n 
where "# n" := (even n) 
with odd : nat -> Set := 
    odS : forall n, #n -> ! S n 
where "! n" := (odd n).