由于 Coq 具有强大的类型推断算法，我想知道我们是否可以根据 Notation 的变量为不同的重写“重载”表示法。
作为一个例子，我将借用我的一篇关于在 Coq 中形式化类型语言语义的工作。在这个形式化中，我有类型对和表达式对，我想为它们各自的构造函数使用相同的符号：{ _ , _ }。
Inductive type: Type := ... | tpair: type -> type -> type | ...
Inductive expr: Type := ... | epair: expr -> expr -> expr | ...
Notation "{ t1 , t2 }" := tpair t1 t2
Notation "{ e1 , e2 }" := epair e1 e2
我知道最后一条语句会引发错误，因为符号已经定义；如果有人考虑过它的诡计，或者如果有另一种“官方”的方式来做到这一点，我将不胜感激。
【问题讨论】：
标签： overloading coq notation
重载符号的一种简单方法是使用作用域。事实上，您应该在大多数情况下使用范围，这样您的符号就不会与您可能包含或可能包含您的其他工作的符号混合。
使用范围分隔符，您可以使用 { t1 , t2 }%ty 和 { e1 , e2 }%exp （使用分隔符 ty 和 exp 来消除歧义）。
也就是说，为了利用类型信息，有一个涉及类型类的技巧，即拥有一个带有自己符号的对的通用概念，然后声明它的实例。请参见下面的示例：
Class PairNotation (A : Type) := __pair : A -> A -> A.
Notation "{ x , y }" := (__pair x y).
Instance PairNotationNat : PairNotation nat := {
__pair n m := n + m
}.
Axiom term : Type.
Axiom tpair : term -> term -> term.
Instance PairNotationTerm : PairNotation term := {
__pair := tpair
}.
Definition foo (n m : nat) : nat := { n , m }.
Definition bar (u v : term) := { u , v }.
【讨论】：
≡ (Equiv)、∅ (Empty)、_ !! _ (Lookup)等。一个小的命名问题（这个答案比 stdpp 做得更好）是，对于名为 Equiv 的类型类，您可能认为您具有等价关系的数学属性，而您得到的只是一个符号（格式良好的属性由另一个类型类声明，Equivalence)。