Coq:未从 List 导入的符号

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].