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

Question

我正在阅读Coq 参考手册的第 4 章。根据参考文献描述的打字规则，术语的类型fun x: nat => x是forall x: nat, nat。

\n\n

Assume that E is [nat: Set].\n\n              ...                                 ...\n------------------------------ Prod-Set  ------------------- Var\nE[] \xe2\x8a\xa2 forall x: nat, nat : Set           E[x: nat] \xe2\x8a\xa2 x : nat\n------------------------------------------------------------ Lam\n        E[] \xe2\x8a\xa2 fun x: nat => x : forall x: nat, nat\n

\n\n

然而，当我Check使用 Coq 这个术语时，它被输入为nat -> nat。

\n\n

Welcome to Coq 8.5pl2 (July 2016)\n\nCoq < Check fun x: nat => x.\nfun x : nat => x\n     : nat -> nat\n

\n\n

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

\n

Answer 1

正如其他人所说，箭头确实是一种符号。请参阅Coq 源代码中的theories/Init/Logic.v#L13 ：

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

该文件由 Prelude 加载，您可以使用 with 来避免它-noinit。