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 

これらの2つのタイプは同じですか？その場合、矢印にはバインドされた変数の名前が隠されていますか？

Answer 1

fun x: nat => xの実際のタイプは、タイプに依存しないため、nat -> natです。矢印はforall _:nat, natのシンタックスシュガーです。ボディのタイプはxの値に依存せず、ボディ自体はxを使用しています。依存関係のタイプの例はvectorです。

vector A nは、タイプAの要素を含む長さnのリストのタイプです。それは、入力として2つの整数nとm、それぞれのサイズnとmの二つのベクトルを取り、それらを連結

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

：の2つのベクトルを連結concat機能を考えてみましょう。今回はタイプのconcatはnとmの値に依存するため、名前を付けて->の代わりにforallを使用する必要があります。 nat -> nat -> vector n A -> ...を書き込もうとすると、変数nは正しくバインドされません。他の人は、矢印が実際の表記であると述べてきたように

Answer 2

、以下を参照してください。このファイルはプレリュードによってロードされるhttps://github.com/coq/coq/blob/trunk/theories/Init/Logic.v#L13

は、あなたが-noinitとしてそれを避けることができます。