Coq：符号未从列表中导入

Question

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

Require Import List.
Check [1].

这会导致以下错误消息：

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

所以基本上这个符号没有被识别为一个有效的构造函数。 相比之下，我可以使用 Bool 中的||。

我被难住了。请救救我！

Answer 1

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

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