在某些Coq理论中，（a：b）c和[a：b] c是什么意思，它的定义在哪里？
|
我看到了一个非常奇怪的语法：（type：2中的type2和表达式中的[name：type] expr，看起来像Pi和Lambda的替代语法，但是经过几个小时的搜索，我在文档中没有找到任何内容， 一切都是徒劳。
它是什么意思，在哪里定义？
（很抱歉，我已丢失示例用法的链接）
没有找到相关结果
已邀请:
1 个回复
箩冀娥
是lambda抽象，现在写为。阅读旧理论时的另一件重要的事情是函数应用程序需要括号并且具有较低的优先级：最高为V7时，表示，表示。