Coq：符号未从列表导入

Question

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

Require Import List.
Check [1].

这会导致以下错误消息：

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

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

我很困惑。请救救我！

Answer 1

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

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