精益4是懒惰还是严格？

Question

Lean 4 是一种纯粹的函数式编程语言，但它是惰性的（如 Haskell）还是严格的（如 Idris）？这意味着什么？有没有办法选择加入（或选择退出）懒惰？

Answer 1

Lean 4 是一种像 Idris 一样严格的语言。