In the "Typing rules" section of the coq reference manual, a note says "We may have 饾梾饾柧饾棈 饾懃:=饾憽:饾憞 饾梻饾棁 饾憿 well-typed without having ((位饾懃:饾憞. 饾憿) 饾憽) well-typed (where 饾憞 is a type of 饾憽). This is because the value 饾憽 associated with 饾懃 may be used in a conversion rule (see Section Conversion rules)."
There is a reduction rule that replaces a let-bound variable with its definition (this is called delta-reduction in the Conversion Rules section of the manual).
So for example, if you have an expression let n := 3 in body
, and somewhere in body
you had an place where an expression of type "vector of length 3" was required, but you wrote an expression of type "vector of length n", then the type checker will automatically unfold the definition of n
. On the other hand, the body of a lambda-expression is type-checked independently, so if you have (fun n => body) 3
, then the type checker will leave n
unexpanded.
Here's a code snippet illustrating the difference:
Require Vector.
Section example.
Variable A : Type.
Variable f : Vector.t A 3 -> unit.
Check
let n := 3 in
(fun (x: Vector.t A n) => f x). (* This type checks. *)
Fail Check
(fun n =>
(fun (x: Vector.t A n) => f x)) (* This gives a type error. *)
3 .
End example.