在 Coq 中添加新符号的问题

Question

我正在尝试定义一个新的符号范围并在 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 没有给出任何错误。

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

Answer 1

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

Declare Scope myHoTT_scope.
Delimit Scope myHoTT_scope with my.

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

此后该符号确实被 Locate 找到并且可以与 %my 定界符一起使用。（请注意，对我来说，Locate 也会找到符号，即使我没有将它放在 myHoTT_scope 中也是如此。）

Answer 2

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

Problems adding new notation in Coq