opérateurs Surcharger dans les notations Coq

Question

J'aimerais créer des notations pour plusieurs types de jugements, par exemple pour une relation de frappe et sous-typage:

Reserved Notation "Г '⊢' t '∈' T" (at level 40). 
Reserved Notation "Г '⊢' T '<:' U" (at level 40). 

Inductive typing_relation : context -> term -> type -> Prop := ... 
where "Γ '⊢' t '∈' T" := (typing_relation Γ t T). 

Inductive subtyping_relation : context -> type -> type -> Prop := ... 
where "Г '⊢' T '<:' U" := (subtyping_relation Γ T U). 

Si je comprends bien, Coq ne permettra pas à cela parce que l'opérateur ⊢ est surchargé dans ces définitions.

Comment pourrais-je faire Coq en déduire la définition d'un opérateur surchargé (dans ce cas, ⊢) sur la base des types de ses arguments (par exemple term vs type) (et/ou sur la base des autres opérateurs qui font partie de la notation, par exemple ∈ par rapport à <:)?

(Notez que l'utilisation des symboles différents ne serait pas une option, parce que mon programme Coq définit plusieurs dactylographie et les relations de sous-typage.)

EDIT: Voici un exemple minimal:

Inductive type : Type := 
    | TBool : type. 

Inductive term : Type := 
    | tvar : nat -> term. 

Definition context := nat -> (option type). 

Reserved Notation "G '⊢' t '∈' T" (at level 40). 

Inductive typing_relation : context -> term -> type -> Prop := 
| T_Var : forall G x T, 
     G x = Some T -> 
     G ⊢ tvar x ∈ T 
where "G '⊢' t '∈' T" := (typing_relation G t T). 

Reserved Notation "G '⊢' T '<:' U" (at level 40). 

Inductive subtype_relation : context -> type -> type -> Prop := 
    | S_Refl : forall G T, 
     G ⊢ T <: T 
    where "G '⊢' T '<:' U" := (subtype_relation G T U). 

Il en résulte l'erreur:

Syntax error: '<:' or '∈' expected after [constr:operconstr level 200] (in [constr:operconstr]). 

Answer 1

la raison est que vous ne pouvez pas utiliser <: comme ça, parce que <: est déjà défini comme Coq de typecast notation. Il agit comme si elle était définie comme si

Reserved Notation "t <: T" (at level 100, right associativity). 

La situation est analogue à celle décrite dans le manuel de référence Coq (§12.1.3):

In the last case though, there is a conflict with the notation for type casts. This last notation, as shown by the command Print Grammar constr. is at level 100. To avoid x : A being parsed as a type cast, it is necessary to put x at a level below 100, typically 99.

Voici une solution possible à votre situation:

Reserved Notation "G '⊢' t '∈' T" (at level 40, t at level 99). 
Reserved Notation "G '⊢' T '<:' U" (at level 40, T at level 99).