Coqの予約表記の複数のWhere-clause？

Question

私はwithを使って宣言された相互誘導データ型をたくさん持っています。定義している間に使用できるそれぞれについてNotationを定義したいと思います。

私はReserved Notationsとwith句を認識していますが、相互誘導型のすべてに使用できる複数の表記法を定義する構文を理解することはできません。

where句に複数の表記を定義することはできますか？もしそうなら、誰かが私が見ることのできる例がありますか？

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