Coq中的构造函数是什么？

Inductive naturals : Type :=
   | Z : naturals
   | N : naturals -> naturals.

说以下事情：

Z

是

naturals

的类型 当

e

是

naturals

的类型时，

N e

是

naturals

的类型。 应用

Z

或

N

是创造自然的唯一两种方法。当给予任意自然时，你知道它是由一个或另一个制成的。 两个术语

e1

和

e2

类型

naturals

是相等的，当且仅当它们都是

Z

或者它们分别是

N t1

和

N t2

且

t1

等于

t2

。 您可以看到这些规则如何推广到任意归纳类型定义。通常，在

t

类型的任意归纳类型定义中： 将构造函数应用于正确类型的参数会产生类型为

t

的术语; 任何类型

t

的术语是应用其中一个与

t

类型相关的构造函数的结果;换句话说，给定一个类型为

t

的词，可以假设它是应用

t

的一个构造函数的结果; 类型

t

的两个术语只有在将相同的构造函数应用于相同的参数时才会相等。 （旁注：当类型定义适用于

Z

和

N

形状的构造函数时，这些属性或多或少完全符合Peano的自然数公理。这就是为什么名为

nat

的类型在Coq中预先定义了这些形状的构造函数用于表示自然数字。这种类型接受特殊处理，因为它很快就会很难以操纵原始形式，但特殊处理只是为了方便。）     

在类型理论中，（类型）构造函数只是一种从现有构造函数构造新类型的方法（http://en.wikipedia.org/wiki/Type_constructor）。 在你对nat的归纳定义中，S是一个构造函数，因为（如果你看一下签名）它需要一个nat并产生另一个nat。 例如，一对nat的类型构造函数将是：

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

Check P (S (O)) (S(S(O))).