在 Coq 中添加新符号的问题答案

【问题标题】：Problems adding new notation in Coq在 Coq 中添加新符号的问题
【发布时间】：2022-01-31 17:39:36
【问题描述】：

我正在尝试定义一个新的符号范围并在 Coq 中将符号添加到此范围。我正在遵循 Coq 手册 (https://coq.inria.fr/refman/user-extensions/syntax-extensions.html) 中此页面的指导。

我用

定义了我的新范围

Declare Scope myHoTT_scope.
Delimit Scope myHoTT_scope with my.

稍后我想将“*”作为中缀运算符添加到范围。我这样做

Infix "*" := concat (at level 40 , left associativity) : myHoTT_scope.

其中 concat 是一个已定义的函数。 Coq 接受所有这些。它不会引发错误或警告。但是，如果我运行

Locate "*".

唯一返回的是 type_scope 和 nat_scope 中“*”的定义。另外，如果我尝试

Check (p * q)%my.

我刚刚收到错误，指出 p 应该是 nat 类型。我不知道为什么 Coq 似乎没有采用这种新符号。我按照信中的说明进行操作，Coq 没有给出任何错误。

**编辑**，我发现了问题。我将新符号的定义隐藏在 Section 内，因此无法从 Section 外部访问它的定义。我想不可能从一个部分中定义全局符号？

【问题讨论】：

您还需要在Infix 符号的末尾添加: myHoTT_scope。但是很奇怪Locate 没有发现它，但我认为我们需要更多的上下文来解决它。有一个可重现的例子会很棒。
哎呀，这是我帖子中的错字。我其实有|| : myHoTT_scope ||在 Coq 代码中。
（您的更正版本）代码对我来说很好用。你有没有在一个新文件中测试过这个（可能不是concat）？如果它在没有任何周围上下文的情况下工作正常，请尝试找到将其弄乱的上下文并分享它。如果它在新文件中不起作用，请告诉我们您使用的是哪个版本的 Coq 以及其他相关信息，以便我们尝试重现它。
感谢@ana-borges 我做到了，并意识到我在一个部分内有中缀行，因此符号不能位于该部分之外。

标签： coq

【解决方案1】：

正如您自己发现的那样，确实不能将部分内的新符号强制为全局的。至少，这是我从参考手册here 中了解到的。并且尝试将 export 和 global 属性添加到符号命令确实失败了。

【讨论】：

【解决方案2】：

您从未说过* 应该在您的新范围内。您必须在符号声明中对其进行精确说明。

Declare Scope myHoTT_scope.
Delimit Scope myHoTT_scope with my.

Infix "*" := concat (at level 40 , left associativity) : myHoTT_scope.

之后，Locate 确实找到了该符号，并且可以与 %my 分隔符一起使用。（请注意，对我来说，Locate 也能找到符号，即使我没有把它放在 myHoTT_scope 中。）

【讨论】：