问Coq:不从列表导入的符号
EN

Stack Overflow用户

提问于 2019-04-02 06:54:36

回答 1查看 808关注 0票数 4

标题很不言自明。我想对列表使用标准的[]和++表示法。但即使在导入之后，它们也无法识别。请参见以下代码。

Require Import List.
Check [1].

这将导致以下错误消息：

Syntax error: [constr:lconstr] expected after 'Check' (in [vernac:query_command]).

因此，基本上，该表示法未被识别为有效的构造函数。相比之下，我可以使用Bool中的||。

我被难住了。请救救我！

回答已采纳

发布于 2019-04-02 08:08:51

列表符号隐藏在两层模块中：

Require Import List.
Import ListNotations.
Check [1].

票数 4

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/55464678

复制

相似问题

问Coq:不从列表导入的符号EN