Могу ли я использовать обозначение для индуктивного типа для определения этого типа в 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. Вот код, который работает:

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 на следующий уровень (49), так что <: получает анализируется с |-, а не впитывается в x.