Несколько мест для зарезервированных обозначений в Coq?

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