我看到了一个非常奇怪的语法:类型中的 (name:type1) type2 和表达式中的 [name:type] expr，看起来像是 Pi 和 Lambda 的替代语法，但几个小时后我在文档中没有找到任何内容苦苦寻找，一切都是徒劳。
它是什么意思以及它是在哪里定义的？ (抱歉，我丢失了示例用法的链接)
最佳答案
您一直在阅读为旧版本 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) 意味着 (f (x=y))和 ([x:nat]y z) 表示 (([x:nat]y) z)。
关于syntax - 什么意思(:b) c and [a:b] c in some Coq theories and where is it defined?，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/5667804/