在某些 Coq 理论中 (a:b) c 和 [a:b] c 意味着什么？它在哪里定义？
我看到了一个非常奇怪的语法：类型中的 (name:type1) type2 和表达式中的 [name:type] expr ，看起来像是 Pi 和 Lambda 的替代语法，但经过几个小时的搜索，我在文档中没有找到任何内容，一切都是徒劳的。
它是什么意思以及它的定义在哪里？ （抱歉，我丢失了示例用法的链接）
I have seen a very strange syntax: (name:type1) type2 in type and [name:type] expr in expressions, looks like alternate syntax for Pi and Lambda, but I haven't found anything in documentation after several hours of searching, all in vain.
What is it means and where it is defined?
(Sorry I've lost link to example usage)
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
您一直在阅读为旧版本 Coq 编写的理论。 V8.0 对语法进行了重大修改。 V8.0 附带了一个将 V7 理论翻译成 V8 的工具，效果非常好；该工具已从后续版本中删除。
您可以在论文从 Coq V7 到 V8 的翻译中查看更改回顾< /a>.
特别地，
(a:b) c是一个通用量化，现在写成forall a:b, c；[a:b] c是一个 lambda 抽象，现在写成fun a:b =>; c.阅读旧理论时另一个重要的事情是函数应用程序需要括号并且优先级较低：直到 V7，(fx = y)意味着(f (x=y))和([x:nat]yz)表示(([x:nat]y) z)。You've been reading a theory written for an older version of Coq. The syntax got a major rehaul with V8.0. V8.0 shipped with a tool to translate V7 theories into V8, which worked pretty well; the tool was dropped from subsequent releases.
You can see a review of changes in the paper Translation from Coq V7 to V8.
In particular,
(a:b) cis a universal quantification, now writtenforall a:b, c;[a:b] cis a lambda abstraction, now writtenfun a:b => c. Another important thing when reading old theories is that function application required parentheses and had low precedence: up to V7,(f x = y)meant(f (x=y))and([x:nat]y z)meant(([x:nat]y) z).