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