Datatype.nat对nat？

Question

问题是，我在Coq中声明了一个归纳函数，并希望对其进行测试。但是，我的Check行出现了一个错误：

Inductive natprod : Type :=
   pair : nat -> nat -> natprod.

Check pair(3 5).

以下是错误：

Error: Illegal application (Non-functional construction): 
The expression "3" of type "Datatypes.nat"
cannot be applied to the term
 "5" : "Datatypes.nat"

我真的不明白问题出在哪里？Datatype.nat和nat的区别是什么？

P.S.：我为"nat“(也叫"Inductive nat")写了一个归纳函数，这有什么问题吗？

Answer 1

pair是nat -> nat -> natprod类型的函数。

因此，要应用它，需要使用函数应用程序语法：

Definition threefive := pair 3 5.

因此，要测试它的类型：

Check (pair 3 5).

nat和Datatypes.nat是相同的类型。Coq只是在某些消息中变得更详细，以避免混淆(它告诉您“数据类型模块中定义的nat”，以防您在其他地方定义了另一个版本.)

我想这条消息的出现是因为您定义了自己的nat，因此如果您定义了自己的，您可能会遇到麻烦：

Check (pair 3 5).

因为3和5是Datatypes.nat的一部分，而不是您创建的nat类型。

因此，您应该使用自己的nat类型的构造函数。