Question: strong normalization in Lean

Stream: lean4

[Yuri de Wit]

I was a bit surprised (not that my surprise means much) when I read in "An Abstract Machine for Strong Call by Need" that "the current version of the Coq proof assistant employs an abstract machine that uses a lazy strategy to fully normalize terms".

Is the (strong) normalization strategy used in Lean4 also lazy/call-by-need? Or is it strict/call-by-value?

[Mario Carneiro]

It's not exactly the call by need algorithm, but it is essentially a lazy algorithm

[Mario Carneiro]

(this is in contrast to the VM / compiler, which is strictly call by value)

[Mario Carneiro]

This is because it's not really an evaluation strategy, it is doing unification