Coq中Record定义使用自定义保留符号报错的技术咨询

嘿，我来帮你解决这个Coq符号定义的报错问题！

你遇到的Error: Unknown interpretation for notation "_ +' _"，根源是符号定义的顺序不对：在你原来的代码里，commute字段先使用了a +' b这个符号，但解释这个符号的where子句是放在commute的后面——Coq在解析commute的命题时，还没处理到where的符号绑定，自然找不到这个符号的解释。

给你两种可行的解决方法：

方法一：先定义Record，再绑定符号 #

这种方式更直观，先完成Record的结构定义，再把符号关联到add字段：

Reserved Notation "A +' B" (at level 80).

Record foo T := {
  add : T -> T -> T;
  commute a b : add a b = add b a
}.

(* 把符号绑定到foo的add字段 *)
Notation "a +' b" := (add a b) (at level 80).

之后你在后续的代码里，就可以用a +' b替代add a b来使用了。

方法二：在Record内部提前定义符号 #

如果你想在Record的字段里直接使用自定义符号，可以把where子句放在add字段之后、commute字段之前，让Coq先识别符号再处理命题：

Reserved Notation "A +' B" (at level 80).

Record foo T := {
  add : T -> T -> T;
  where "a +' b" := (add a b);
  commute a b : a +' b = b +' a
}.

这样调整顺序后，Coq在解析commute时已经知道a +' b就是add a b，就不会再报错啦。

补充一句：你一开始用Reserved Notation预留符号优先级的做法是对的，这能避免自定义符号和Coq内置符号的优先级冲突。

内容的提问来源于stack exchange，提问作者larsr