为什么Coq不接受这一点？
Notation "[ d1 , .. , d2 ]" := (addition (multiply ( .. d1 .. ) ten) d2).
递归符号需要遵守相当严格的规则。要重复的模式必须出现两次（这就是Coq知道要重复什么的方式）：一次在孔周围使用d2，一次在终止表达式附近使用d1。您只使用过一次图案，在洞周围使用d2。您需要另一次迭代，围绕一些zero（如列表符号中的nil）。
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).