Is Lean 4 lazy or strict?

Question

Lean 4 is a purely functional programming language, but is it lazy (like Haskell) or strict (like Idris) and what are the implications of this? Is there a way to opt-in (or opt-out) of laziness?

Answer 1

Lean 4 is a strict language like Idris.