Coq中保留符號的多個Where-clause？

Question

我有一堆使用with聲明的相互感應的數據類型，我想爲它們定義一個Notation，我可以在定義它們時使用它們。

我知道Reserved Notations和with子句，但我無法弄清楚定義多種符號的語法，這些符號可用於我所有的相互歸納類型。

是否可以在where子句中定義多個Notation，如果有，是否有人可以看到我的例子？

Answer 1

一個例子：

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