'Are arrows in Coq aliases of universal quantifications?

I'm reading chapter 4 of the reference manual of Coq. According to the typing rules described by the reference, the type of term fun x: nat => x is 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

However, when I Check this term by Coq, it is typed nat -> nat.

Welcome to Coq 8.5pl2 (July 2016)

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

Are these two types same ones? If so, do arrows have hidden names of bound variables?

coq


Solution 1:[1]

As others have said arrow is indeed a notation. See theories/Init/Logic.v#L13 in the Coq sources:

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

This file is loaded by the Prelude, you can avoid it with with -noinit.

Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source
Solution 1 Jo Liss

Related Questions