Coq: исправление рекурсивной нотации

Question

Ниже приведена простая рабочая рекурсивная запись:

Universe ARG. Definition ARG := Type@{ARG}.
Parameter X: ARG.
Notation A := (fun x:ARG->ARG => fun y:x X => y).
Parameter P: ARG -> ARG.
Parameter s: P X.
Notation "[ x .. z u ]" := (x P .. (z P u) .. ) (at level 5, z, u at next level).
Check (A P (A P (A P s))). (* [A A A s]: P X *)
Print Grammar constr.
(*| "5" RIGHTA
  [ "["; NEXT; LIST1 NEXT; NEXT; "]"
  | "["; NEXT; NEXT; "]" ]*)
Check [A A A s]. (* Syntax error: [constr:operconstr] or [constr:operconstr] expected (in [constr:operconstr]). *)

Как видите, Coq признает A P (A P (A P s)) как [A A A s]: P X но не могу разобрать [A A A s], В чем проблема, в чем ее решение?

РЕДАКТИРОВАТЬ: Coq, кажется, требует некоторых "вспомогательных средств" здесь. Например, следующие работы:

Notation "( x .. z [ u ] )" := (x P .. (z P u) .. ) (at level 5, z at next level).
Check (A A A [s]): P X.

Поскольку я хотел бы избавиться от внутренней нотации, вопрос остается открытым

Answer 1

Проблема в том, что Coq <= 8.7 не поддерживает рекурсивные обозначения вида x .. y z очень хорошо, и исправление заключается в том, чтобы загрузить Coq master или дождаться Coq 8.8. Исправление Хьюго Гербелина, озаглавленноеAdding support for recursive notations of the form "x , .. , y , z", был объединен 1 августа 2017 года.