I'd like to create notations for several kinds of judgements, for example for a typing and subtyping relation:
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).
As I understand, Coq will not allow this because the ⊢
operator is overloaded in those definitions.
How could I make Coq infer the definition of an overloaded operator (in this case, ⊢
) based on the types of its arguments (e.g. term
vs type
) (and/or based on the other operators that are part of the notation, e.g. ∈
vs <:
)?
(Note that using different symbols would not be an option, because my Coq program defines several typing and subtyping relations.)
EDIT: Here is a minimal example:
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).
This results in the error:
Syntax error: '<:' or '∈' expected after [constr:operconstr level 200] (in [constr:operconstr]).