在 [constr:operconstr] 之后使用预期的 3 符号表示法 [constr:operconstr]

Question

假设我有一个关系及其自反和传递闭包（n 计算 "transitive steps" 的数量：

Variable A: Type.

Inductive Relation: A -> A -> Prop :=
| rel: forall (a b: A), Relation a b.

Notation "a --> b" := (Relation a b) (at level 50).

Inductive Refl_Trans_Rel: A -> A -> nat -> Prop :=
| zero_step: forall a b, a --> b -> Refl_Trans_Rel a b 0
| n_steps: forall a b c n, a --> b /\ Refl_Trans_Rel b c n
    -> Refl_Trans_Rel a c (S n).

现在，我想要一个类似于 a --> b:

的符号

Notation "a -->^ n b" :=
  (Refl_Trans_Rel a b n) (at level 50, n at next level, b at next level).

打印没问题：Check forall a b n, Refl_Trans_Rel a b n.确实打印：

forall (a b : A) (n : nat), a -->^ n b
 : Prop

但是，当我想自己使用表示法时，出现了问题：

Check forall a b n, a -->^ n b.

失败：

Syntax error: [constr:operconstr] expected after [constr:operconstr]
  (in [constr:operconstr]).

知道为什么会失败吗？

P.S.: 随意编辑更精确的标题，因为我不知道原因，我没有更好的标题。

Answer 1

Coq 似乎试图将 a -->^ n b 中的 n b 部分解析为函数应用程序。克服这个困难的一种方法是将 n 放在较低的级别，如下所示：

Notation "a -->^ n b" := (Refl_Trans_Rel a b n) (at level 50, n at level 9).
Check forall (a b : A) (n : nat), a -->^ n b.

另一种选择是在 b 和 n 之间放置一个分隔符：

Notation "a --> b # n" := (Refl_Trans_Rel a b n) (at level 50).
Check forall (a b : A) (n : nat), a --> b # n.

您可以了解有关符号和解析级别的更多信息。

在 [constr:operconstr] 之后使用预期的 3 符号表示法 [constr:operconstr]

Using a 3 symbols notation [constr:operconstr] expected after [constr:operconstr]

notation

coq