在勒柯克运算符重载符号

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