Kann ich eine Notation für einen induktiven Typ verwenden, um diesen Typ in Coq zu definieren?

Question

Angenommen, ich habe so etwas wie dies:

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. 

Und eine Notation definiert:

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

Gibt es eine Möglichkeit, diese Notation in Rahmen für die Definition von SubtypeOf bringen kann, so ich könnte so etwas tun:

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

Aufbauend auf ejgallego Kommentar gibt es doc für Reserved Notations und a where clause for inductives. Hier ist der Code, das funktioniert:

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

Bitte beachte, dass wir x auf der nächsten Ebene stellen müssen (49), so dass die <: mit |- analysiert wird, anstatt in x absorbiert wird.