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

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

ltac coq list

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

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

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

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

2 回复 | 直到 7 年前

Li-yao Xia 7 年前

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

(x, y, z)

去糖剂

pair (pair x y) z

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

Carl Patenaude Poulin 7 年前

通过与亚当的私人通信:

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

推荐文章

Mei Zhang · 定义“依赖类型”模函子

8 年前

Jason Hu · 参见Ltac中的Hintbase

8 年前

lllllllllllll · 通过两个实现对阶乘程序进行Coq验证

8 年前

MikkelBybjerg · 如何延迟lambda评估,以便替换lambda

8 年前

user9335697 · 实例化参数以评估函数定义

8 年前

Jian Wang · Coq中的背景目标、搁置目标和放弃目标是什么?

8 年前

Pablo Inostroza · 有没有可能表达一个定理,说明应用了哪些构造函数?

8 年前

jmite · Coq:在校样脚本编写期间查看校样术语

8 年前

ConfusedFormalizer · a是怎样的。vo文件的结构是否便于coqchk使用?

8 年前

Siddharth Bhat · 查看所有已安装的库以及如何在Coq中导入它们

8 年前