Coq 中的对定义类型为“(Set * Set)%type”，而预期类型为“Type”

Question

我正在阅读 Software Foundations(*) 并且在 Coq 中定义类型时遇到问题：在下面的示例中，我尝试进行 2 个类型定义。t1是自然数列表，并且t2是一对自然数。

第一个定义t1被 Coq 接受，但定义t2被拒绝并显示错误消息：

该术语(nat, nat)具有类型，(Set * Set)%type而预期具有类型Type。

我不太明白出了什么问题以及这条消息的含义。定义有什么问题t2？

  Definition t1 : Type := list nat.
  Definition t2 : Type := pair nat nat.

(*) http://www.cis.upenn.edu/~bcpierce/sf/Lists.html#lab58

Answer 1

不，pair是构造函数，prod是类型。

Print prod.
Check prod.
Check @pair.

Definition t1 : Type := list nat.
Definition t2 : Type := prod nat nat.
Definition t2' : Type := (nat * nat)%type.