'Is Lean 4 lazy or strict?

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?



Solution 1:[1]

Lean 4 is a strict language like Idris.

Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source
Solution 1 Leonardo de Moura