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