Coq의 화살표는 보편적 인 정량화의 별칭입니까?

Question

나는 chapter 4 of the reference manual of Coq을 읽고 있습니다. 참고 문헌에서 설명한 타이핑 규칙에 따라 fun x: nat => x이라는 용어의 유형은 forall x: nat, nat입니다. I Check COQ하여이 용어는, 그것은 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 

.

Welcome to Coq 8.5pl2 (July 2016) 

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

이 두 유형은 같은 종류입니까? 그렇다면 화살표는 바운드 변수의 숨겨진 이름을 갖고 있습니까?

Answer 1

fun x: nat => x의 실제 유형은 유형 종속성이 없으므로 nat -> nat입니다. 화살표는 forall _:nat, nat의 구문 설탕입니다. 본문의 형식은 x의 값에 의존하지 않고 본문 자체 만 x을 사용합니다. 종속성 유형의 예는 vector입니다.

vector A n은 유형이 A 인 n의 목록 유형입니다. 의 두 벡터를 연결할 concat 기능을 살펴 보자 : 그것은 입력이 개 정수, n 및 m, 각각의 크기 n 및 m 두 벡터로한다

concat : forall n m: nat, vector n A -> vector m A -> vector (n + m) A 

을 연결할. 이번에 유형은 n과 m의 값에 따라 달라 지므로 이름을 지정하고 -> 대신 forall을 사용해야합니다. nat -> nat -> vector n A -> ...을 쓰려고하면 변수 n이 바운드되지 않습니다. 다른 사람들이 화살표가 참으로 표기입니다 말했듯이

Answer 2

, 참조 :이 파일은 전주곡에 의해로드됩니다 https://github.com/coq/coq/blob/trunk/theories/Init/Logic.v#L13

, 당신은 -noinit과 함께 피할 수 있습니다.