Coq 泛型中的花括号

Question

下面的代码给出了一个错误：

Inductive mylist {A : Set} : Set :=
| mylist_Nil
| mylist_Cons : A -> mylist A -> mylist A.

错误是“Set”类型的“mylist A”不能应用于术语“A”：“Set”。如果我将 "{A:Set}" 更改为 (A:Set) 那么它工作正常。

花括号是什么意思？谢谢！

Answer 1

通常，使用括号声明参数。花括号用于隐式参数。隐式参数不像通常那样传递给函数和类型声明；相反，Coq 类型检查器试图从上下文中找出它们应该是什么。

可以强制不断采取各种参数指定与@标志，就像这样：@mylist A。

对于像 那样的泛型类型mylist，Coq 没有足够的上下文来推断A参数应该是什么，因此通常最好用括号显式声明这些参数。

该Coq的用户手册，对隐含参数的更多信息。