coq - Coq 中的箭头是通用量化的别名吗？

Question

我正在阅读 chapter 4 of the reference manual of Coq .根据引用文献描述的打字规则，fun x: nat => x 的类型为forall x: nat, nat。

Assume that E is [nat: Set].

              ...                                 ...
------------------------------ Prod-Set  ------------------- Var
E[] ⊢ forall x: nat, nat : Set           E[x: nat] ⊢ x : nat
------------------------------------------------------------ Lam
        E[] ⊢ fun x: nat => x : forall x: nat, nat

但是，当我通过 Coq Check 这个术语时，输入的是 nat -> nat。

Welcome to Coq 8.5pl2 (July 2016)

Coq < Check fun x: nat => x.
fun x : nat => x
     : nat -> nat

这两种类型是一样的吗？如果有，箭头是否隐藏了绑定(bind)变量的名称？

Answer 1

正如其他人所说，箭头确实是一种符号。见 theories/Init/Logic.v#L13在 Coq 来源中:

Notation "A -> B" := (forall (_ : A), B) : type_scope.

这个文件是由 Prelude 加载的，你可以用 -noinit 来避免它。