我看到了一个非常奇怪的语法：(name:type1) type2 in type 和 [name:type] expr 在表达式中，看起来像是 Pi 和 Lambda 的替代语法，但经过几个小时的搜索，我在文档中没有找到任何东西，一切都是徒劳。
它是什么意思，在哪里定义？（对不起，我失去了示例用法的链接）
问问题
102 次
1 回答
4
您一直在阅读为旧版 Coq 编写的理论。V8.0 对语法进行了重大改进。V8.0 附带了一个将 V7 理论转换为 V8 的工具，效果很好；该工具已从后续版本中删除。
您可以在论文Translation from Coq V7 to V8中查看对更改的评论。
特别是，(a:b) c是一个普遍的量化，现在写成forall a:b, c；[a:b] c是一个 lambda 抽象，现在写成fun a:b => c. 阅读旧理论时另一个重要的事情是函数应用需要括号并且优先级低：直到 V7，(f x = y)mean(f (x=y))和([x:nat]y z)mean (([x:nat]y) z)。
于 2011-04-14T22:21:46.157 回答