不要在 coq 中导入符号答案

【问题标题】：Do not import notations in coq不要在 coq 中导入符号
【发布时间】：2018-03-19 20:15:15
【问题描述】：

我有两个定义相同符号的外部模块（其来源最好不要交替）。这样做的结果是，由于此错误，我现在无法同时导入两个模块：

Error: Notation _ ~ _ is already defined at level 27 with arguments at level 27,
at next level while it is now required to be at level 50 with arguments at next level,
at next level.

有什么办法吗？我想要么不从一个模块导入符号，要么只进行选择性导入。但是，翻阅文档并没有说明太多。

我有机会看过吗？或者您会推荐什么解决方案？

【问题讨论】：

标签： import module coq notation

【解决方案1】：

不幸的是，简短的回答是否。 Upstream 意识到了这个限制，并且在未来的某个时候（Coq 8.9？），您希望能够使用“解析表”来做到这一点。

但是，有一个可接受的解决方法：使用部分来限制您的导入范围。想象一下模块 a b 定义了一个冲突的符号，那么你可以这样做：

Require a b.

Section WithNotationA.
Import a.
...
End WithNotationA.

Section WithNotationB.
Import b.
...
End WithNotationB.

【讨论】：