在某些Coq理论中，a：bc和[a：b] c是什么意思，它的定义在哪里？

问题描述

| 我看到了一个非常奇怪的语法：（type：2中的type2和表达式中的[name：type] expr，看起来像Pi和Lambda的替代语法，但是经过几个小时的搜索，我在文档中没有找到任何内容， 一切都是徒劳。 它是什么意思，在哪里定义？ （很抱歉，我已丢失示例用法的链接）     

解决方法

您正在阅读为较旧版本的Coq编写的理论。 V8.0对语法进行了重大改进。 V8.0附带了将V7理论转换为V8的工具，效果很好。该工具已从后续版本中删除。 您可以在论文《从Coq V7到V8的转换》中查看对更改的评论。 特别地，“ 0”是通用量化，现在写为“ 1”；

[a:b] c

是lambda抽象，现在写为

fun a:b => c

。阅读旧理论时的另一件重要的事情是函数应用程序需要括号并且具有较低的优先级：最高为V7时，

(f x = y)

表示

(f (x=y))

，

([x:nat]y z)

表示

(([x:nat]y) z)

。