귀납적 유형에 대한 표기법을 사용하여 Coq에서 해당 유형을 정의 할 수 있습니까?

Question

한다고 가정 내가있어이 같은 :

Inductive SubtypeOf : 
    Gamma -> UnsafeType -> Type -> Set := 
| SubRefl : 
    forall (gamma : GammaEnv) (u : UnsafeType) 
    , SubtypeOf gamma u u 
| SubTrans : 
    forall (gamma : GammaEnv) (u1 u2 u3 : Type) 
    , SubtypeOf gamma u1 u2 
     -> SubtypeOf gamma u2 u3 
     -> SubtypeOf gamma u1 u3. 

그리고 표기법 정의 :

Notation "G |- x <: y " := (SubtypeOf G x y) (at level 50).

내가 SubtypeOf의 정의 범위로이 표기법을 가져올 수있는 방법이 너무 있나요 다음과 같이 할 수 있습니다.

Inductive SubtypeOf : 
    Gamma -> UnsafeType -> Type -> Set := 
| SubRefl : 
    forall (gamma : GammaEnv) (u : UnsafeType) 
    , gamma |- u <: u 
| SubTrans : 
    forall (gamma : GammaEnv) (u1 u2 u3 : Type) 
    , gamma |- u1 <: u2 
     -> gamma |- u2 <: u3 
     -> gamma |- u1 <: u3. 

Answer 1

ejgallego 님의 의견이 확장되면 다음과 같이 표시됩니다. Reserved Notations 및 a where clause for inductives에 대한 설명 <:가 |-를 사용한 구문 분석됩니다 있도록 우리가보다는, 다음 단계 (49)에서 x를 삽입해야합니다

Reserved Notation "G |- x <: y" (at level 50, x at next level). 
Definition UnsafeType := Type. 
Axiom Gamma : Set. 
Notation GammaEnv := Gamma. 
Inductive SubtypeOf : 
    Gamma -> UnsafeType -> Type -> Type := 
| SubRefl : 
    forall (gamma : GammaEnv) (u : UnsafeType) 
    , gamma |- u <: u 
| SubTrans : 
    forall (gamma : GammaEnv) (u1 u2 u3 : Type) 
    , gamma |- u1 <: u2 
     -> gamma |- u2 <: u3 
     -> gamma |- u1 <: u3 
where "G |- x <: y " := (SubtypeOf G x y). 

참고 x에 흡수되고 : 여기에 작동하는 코드입니다.