是否可以在 Coq 中为多个构造函数定义单一符号？如果构造函数的参数类型不同，则可以从中推断出它们。一个最小的（非）工作示例：
Inductive A : Set := a | b | c: C -> A | d: D -> A
with C: Set := c1 | c2
with D: Set := d1 | d2.
Notation "' x" := (_ x) (at level 19).
Check 'c1. (*?6 c1 : ?8*)
在这种情况下，构造函数推断不起作用。也许还有另一种方法可以将构造函数指定为变量？
您可以使用构造函数作为实例创建一个类型类，并让实例解析机制推断要为您调用的构造函数：
Class A_const (X:Type) : Type :=
a_const : X -> A.
Instance A_const_c : A_const C := c.
Instance A_const_d : A_const D := d.
Check a_const c1.
Check a_const d2.
顺便说一句，对于 Coq 8.5，如果你真的想要一个符号' x产生准确的构造函数应用于x，而不是例如@a_const C A_const_c c1，那么您可以使用 ltac-terms 来实现：
Notation "' x" := ltac:(match constr:(a_const x) with
| @a_const _ ?f _ =>
let unfolded := (eval unfold f in f) in
exact (unfolded x)
end) (at level 0).
Check 'c1. (* c c1 : A *)
Check 'd2. (* d d2 : A *)
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
