Why are let binders part of the kernel in Coq/Lean?

Question

I've been looking into the implementations of CIC-based theorem provers - mainly Coq and Lean - and it seems that both of them have let binders as part of the kernel, with their own typing and reduction rules.

I get why let binders are useful, but it seems to me they could just be syntactic sugar: let x:T = y in z --> (fun x:T, z)(y) Is there a type-theoretic reason they're in the kernel as a separate concept, or is it for implementation/software efficiency reasons?

Answer 1

let is not derivable as syntactic sugar in type theory. That only works if types cannot depend on let-defined names. For example, trying to desugar let A : Set = Bool in λ (x : A). not x yields (λ (A : Set) (x : A). not x) Bool which is ill-typed.

We can either add let to core syntax, or unfold all let-s during elaboration. The latter may cause a size explosion in elaboration output, and let-s are very useful in the surface language, so the straightforward solution is to have let as primitive.