Puis-je utiliser une notation pour un type inductif pour définir ce type dans Coq?

Question

Supposons que j'ai quelque chose comme ceci:

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. 

Et une notation définie:

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

Est-il possible que je peux apporter cette notation dans la portée de la définition de SubtypeOf, donc Je pourrais faire quelque chose comme ceci:

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

En étendant le commentaire d'ejgallego, il y a doc une coloration pour Reserved Notations et a where clause for inductives. Voici le code qui fonctionne:

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

Notez que nous devons mettre x au niveau suivant (49), de sorte que le <: obtient parsé avec |-, plutôt que d'être absorbé dans x.