Coq：修复递归符号答案

【问题标题】：Coq: Fixing a recursive notationCoq：修复递归符号
【发布时间】：2017-06-27 21:37:25
【问题描述】：

下面是一个简单的递归符号：

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.

由于我想摆脱内部符号，问题仍然悬而未决

【问题讨论】：

标签： parsing recursion definition coq notation

【解决方案1】：

问题是 Coq x .. y z 形式的递归表示法，解决方法是下载 Coq master，或者等待 Coq 8.8。 Hugo Herbelin's fix, entitled Adding support for recursive notations of the form "x , .. , y , z"，于 2017 年 8 月 1 日合并。

【讨论】：