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