Poly 模块中有 4 个与教会数字相关的练习：
Definition cnat := forall X : Type, (X -> X) -> X -> X.
据我所知，cnat 是一个函数，它接受一个函数 f(x)，它是参数 x 并返回这个参数的值：f(x)。
然后有 4 个例子，分别代表 0、1、2 和 3 用 Church 记谱法表示。
但是如何解决呢？我知道我们必须再次应用该功能。 cnat 返回的值将作为参数。但是如何编码呢？使用递归？
Definition succ (n : cnat) : cnat
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
更新
我试过了：
Definition succ (n : cnat) : cnat :=
match n with
| zero => one
| X f x => X f f(x) <- ?
【问题讨论】：
请记住，Church 数字是两个参数的函数（如果您还计算类型，则为三个）。参数是函数f 和起始值x0。 Church 数字将f 应用于x0 多次。 Four f x0 将对应于 f (f (f (f x0)))，Zero f x0 将忽略 f 而只是 x0。
对于n 的继任者，请记住n 将为您应用任何函数f n 次，因此如果您的任务是创建一个函数，则将一些f 应用于一些x0 @ 987654336@ 次，只需将大部分工作留给教堂数字n，将您的f 和x0 给它，然后再对@987654341 返回的结果应用f 以结束@。
您将不需要任何match，因为函数不是可以进行案例分析的归纳数据类型...
【讨论】：
据我所知，cnat 是一个函数，它接受一个函数 f(x)，它是参数 x 并返回这个参数的值：f(x)。
请注意，cnat 本身并不是一个函数。相反，cnat 是所有此类函数的类型。另请注意，cnat 的元素也将X 作为参数。记住cnat 的定义会有所帮助。
Definition succ (n: cnat): cnat.
Proof.
unfold cnat in *. (* This changes `cnat` with its definition everywhere *)
intros X f x.
在这之后，我们的目标只是X，我们有n : forall X : Type, (X -> X) -> X -> X、X、f和x作为前提。
如果我们将n 应用于X、f 和x（如n X f x），我们将得到X 的元素，但这并不是我们想要的，因为最终结果将再次成为n。相反，我们需要在某个地方多申请一次f。你能看到在哪里吗？有两种可能。
【讨论】：
Qed 不起作用。
:= 的形式中。请注意，证明并不完整，因此您还不能以Qed. 结束它。我只是想让你看看有什么前提和输出类型应该是什么。
您可以通过以下方式为succ 编写Definition：
Definition succ (n : cnat) : cnat :=
fun (X : Type) (f : X -> X) (x : X) => f (n X f x).
【讨论】：