coq - 在 Coq 中编写自然数符号时遇到问题

Question

为什么 Coq 不接受这个？

Notation "[ d1 , .. , d2 ]" := (addition (multiply ( .. d1 .. ) ten) d2).

Answer 1

递归符号需要遵守相当严格的规则。重复的模式必须出现两次（这就是 Coq 知道要重复什么的方式）：一次d2在孔周围使用，一次在终止表达式d1周围使用。你只用过一次你的图案，在洞周围使用。你需要另一个迭代，围绕一些（比如列表的符号）。d2zeronil

Notation "[ d1 , .. , d2 ]" :=
  (addition (multiply .. (addition (multiply zero ten) d1) .. ten) d2).

如果您不想引入零，则可以在括号内至少要求两位数（而不是上面的一位），并将其用作终止表达式。这就像对的符号（在Init/Notations.v手册中也有介绍）。您可以用较低优先级的符号来补充这一点[d0]，但这只是d0没有多大意义。

Notation "[ d0 , d1 , .. , d2 ]" :=
  (addition (multiply .. (addition (multiply d0 ten) d1) .. ten) d2).