6
$\begingroup$

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?

$\endgroup$

1 Answer 1

9
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .