在勒柯克運算符重載符號

Question

我想對幾種判斷創建符號，例如用於打字和子類型關係：

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

據我瞭解，勒柯克不會允許這種情況是因爲⊢操作在這些定義中被重載。

我如何才能讓勒柯克推斷重載運算符的定義（在這種情況下，⊢）的基礎上的類型的參數（如term VS type）（和/或基於被部分其他運營商符號，例如∈ vs <:）？

（請注意，使用不同的符號會不會是一種選擇，因爲我的勒柯克程序定義了幾種類型和子類型的關係。）

編輯：這裏是一個小例子：

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

這導致錯誤：

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

Answer 1

的原因是，你不能使用<:這樣的，因爲<:已經被定義爲勒柯克的typecast notation。它的作用，如果它是像這樣

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

所述的情況是類似於在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.

這裏是您的情況可能的解決方案：

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