coq - 检查cnat。并得到类型返回

Question

全部

我试图理解 SF-LF 书 chp4 中提到的教堂数字。

Definition cnat := forall X : Type, (X -> X) -> X -> X.
Definition one : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => f x.
Check cnat.
Check one.

我得到

cnat
     : Type
one
     : cnat

似乎 cnat 是某种类型，并且同时起作用。怎么可能兼具类型和功能？任何人都可以帮助解释一下吗？

Answer 1

" forall (X : Type)," 语法是一种从由 . 参数化的类型形成类型的方法X。forall (X : Type), (X -> X) -> X -> X是函数的一种类型，给定一个类型X会产生一个类型的值(X -> X) -> X -> X（它本身就是一个函数）。

" fun (X : Type) =>" 语法是一种形成函数的方法，由X. fun (X : Type) (f : X -> X) (x : X) => f x是一个函数，它给定一个类型X产生函数fun (f : X -> X) (x : X) => f x（它本身就是一个函数）。

fun它们的共同点是forall它们都涉及到binders，like (X : Type)(also like (f : X -> X), (x : X))。fun是一种涉及绑定器以形成函数的构造，但并非所有涉及绑定器形成函数forall的构造：是一种涉及绑定器以形成类型的构造。