I found this code on this stackexchange post and I'm confused about why it works. In particular,
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).
In the check, is 42 being bound to A? Doesn't A have to be a type? I tried replacing 42 with things that obviously are types, like 'bool' or 'Type', and those worked too. That makes sense to me. But how does 42 typecheck there?
A
is an implicit argument for Vector
, which (by default) is inherited by the constructor cons
. This is indicated by the curly brackets around A : Type
in Inductive Vector {A : Type} : nat -> Type
.
Thus, in cons n 42 nil
, cons
is applied to some implicit type ?A
, the natural number n
, the element of type ?A
42
and the Vector 0
nil
. Since 42
has type nat
, ?A
can be inferred to be nat
.