感谢软件基金会的电子书，我目前正在学习 coq 。我成功地添加了如下内容：
Definition cnat := forall X : Type, (X -> X) -> X -> X.
Definition plus (n m : cnat) : cnat :=
fun (X : Type) (f : X -> X) (x : X) => n X f (m X f x).
但由于以下错误，我坚持使用 exp：
Definition exp (n m : cnat) : cnat :=
m cnat (mult n) n.
(*
In environment
n : cnat
m : cnat
The term "cnat" has type "Type@{cnat.u0+1}"
while …