Lean Kernel Arena / perf/let-ladder

The declaration to check has type Nat and value

let x₃ := 0; x₃ + (let x₂ := 0; x₂ + (let x₁ := 0; x₁ + (x₃ + (x₂ + (x₁ + 0)))))

shown at n=3: n let bindings, each separated from the next by an addition, over an innermost sum that names every binding.

Substituting a binding into the body before checking it traverses O(n) nodes at each of the n bindings, for Θ(n²) in time and in allocated nodes. Recording the binding and reading it where the body names it costs O(1) per binding, for Θ(n).

The additions are what keep the bindings apart: a run of adjacent lets could be opened by a single substitution; not so here. Nat.add is the only application head, so no beta reduction is involved.

N=2000 in the Lean source.