Coq "Unknown interpretation for notation" 错误

Question

我正在按照 https://www.cis.upenn.edu/~bcpierce/sf/current/Imp.html 中的说明进行操作，并尝试定义一个新符号 |\。（而不是 ||，它在网页中使用但似乎被我的 coq 解释为 OR 运算符）

Reserved Notation "e |\ n" (at level 50, left associativity).

但是 coq 仍然认为 |\ 是未定义的运算符。

Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum : forall n : nat, (ANum n) |\ n.

Error: Unknown interpretation for notation "_ |\ _".

我的 coq 版本是 8.4pl6（2015 年 11 月）。如何让 coq 接受我的新 |\ 运算符？

Answer 1

您需要将 where 子句附加到您的关系定义中，如软件基础中的示例所示：

Reserved Notation "e |\ n" (at level 50, left associativity).

Inductive aexp := ANum : nat -> aexp.

Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum : forall n : nat, (ANum n) |\ n

where "x |\ y" := (aevalR x y).

Coq "Unknown interpretation for notation" 错误

Coq "Unknown interpretation for notation" error

coq