代码之家 › 专栏 › 技术社区 › Carl Patenaude Poulin

为什么Adam Chlipala使用左相关的嵌套元组来表示CPDT中的Ltac列表?

ltac coq list

1

Carl Patenaude Poulin · 技术社区 · 6 年前

x 在列表中 ls ,用左相关的嵌套元组表示。

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

这似乎不典型。列表的尾部不是按惯例放在元组的右边吗?

2 回复 | 直到 6 年前

1

2

Li-yao Xia 6 年前

不知何故,n元组是与左侧相关联的嵌套对:

(x, y, z)

去糖剂

pair (pair x y) z

如果我们想写作,那就是我们得到的 inList x (x, y, z) .

2

3

Carl Patenaude Poulin 6 年前

通过与亚当的私人通信:

不,我想不出有什么办法能比其他版本更喜欢一个版本, 事实上。我只是要为书的那部分做些选择。