list - 为什么 Adam Chlipala 使用左关联嵌套元组来表示 CPDT 中的 Ltac 列表？

Question

通过CpdtTactics.v：

[...]成功当且仅x在 list 中ls，用左关联嵌套元组表示。

Ltac inList x ls := match ls with | x => idtac | (_, x) => idtac | (?LS, _) => inList x LS end.

这似乎不典型。列表的尾部不是按惯例位于元组的右侧吗？

Answer 1

通过与亚当的私人交流：

不，实际上，我想不出任何方式来选择一个版本而不是另一个版本。我只需要为这本书的那一部分做出一些选择。

Answer 2

不知何故，n元组是与左侧关联的嵌套对：

(x, y, z)

脱糖

pair (pair x y) z

如果我们想写的话，这就是我们得到的inList x (x, y, z)。