about loop in Lean

Stream: new members

[li sheng]

I known in functional programming language like Haskell using recursion to realize loops ,while Lisp has a few realizations for loop !
Is it necessary for Lean to have a loop structure,like 'for loop,while loop' or others ? Thanks !

[Eric Wieser]

Lean does not permit writing non-terminating programs (except in meta code), which pretty much rules out while loops. I don't know if we have a meta while loop, but I think it would be straightforward to build one.

[Eric Wieser]

You can do a for loop with docs#list.range and docs#list.map or docs#list.foldl

[li sheng]

I see, Thanks!

[Horatiu Cheval]

Lean4 will introduce a for notation within do that almost makes you feel you are writing in an imperative language: https://leanprover.github.io/lean4/doc/do.html#iteration. But even with that, Lean doesn't use loops in the sense of imperative programs, and everything comes down to recursion, like Eric said.

[li sheng]

Great!Thank you!