[coq中的参数类型

Question

我在此stackexchange post上找到了此代码，我对其工作原理感到困惑。特别是

Inductive Vector {A : Type} : nat -> Type :=
| nil : Vector 0
  | cons : forall n, A -> Vector n -> Vector (S n).

(* This works. *)
Check (let n := 0 in cons n 42 nil).

在支票中，是否将42绑定到A？ A是否必须是类型？我尝试用显然是类型的东西（例如“ bool”或“ Type”）替换42，这些东西也起作用。这对我来说很有意义。但是，如何在那里进行42型检查？

Answer 1

A是implicit argument的Vector，（默认情况下）由构造函数cons继承。这由A : Type中Inductive Vector {A : Type} : nat -> Type周围的大括号表示。

因此，在cons n 42 nil中，cons适用于某些隐式类型?A，自然数n，类型?A 42和Vector 0 nil的元素。由于42的类型为nat，因此可以将?A推断为nat。