Coq符号

Question

我希望使用这些符号来表示谓词测试，如下所示：

Variable A B : Type.

Inductive test : A -> B -> A -> B -> Prop :=
| test1 : forall a1 a2 b1 b2,
    a1 \ b1 || a2 \ b2
where "c1 '\' st '||' c2 '\' st'" := (test c1 st c2 st')
.

但是，Coq有一个错误：

​

为什么这个表示法在Coq中不能被接受？

Answer 1

这个表示法被接受了，实际上是Coq错误地解析了test1定义中使用的表示法。要正确解析这个表示法，您需要调整其术语的解析级别。您可以使用保留表示法来实现这一点，因为这些用于归纳中的符号的where子句不支持配置表示法的语法：

Variable A B : Type.

Reserved Notation "c1 '\' st '||' c2 '\' st'" (at level 40, st at next level, c2 at next level, no associativity).

Inductive test : A -> B -> A -> B -> Prop :=
| test1 : forall a1 a2 b1 b2,
    a1 \ b1 || a2 \ b2
where "c1 '\' st '||' c2 '\' st'" := (test c1 st c2 st')
.

对于哪些解析级别工作得很好，我没有很好的直觉(上面有40条是任意的)，所以我能给出的最好的建议是进行实验，如果在某个地方分析不正确，那么就尝试调整级别。