coq - 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 user manual有更多关于隐式参数的信息。