Zulip Chat Archive

Stream: new members

Topic: about loop in Lean

li sheng (Jul 03 2021 at 09:20):

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 (Jul 03 2021 at 09:23):

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 (Jul 03 2021 at 09:24):

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

li sheng (Jul 03 2021 at 09:25):

I see, Thanks!

Horatiu Cheval (Jul 03 2021 at 09:37):

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 (Jul 03 2021 at 09:41):

Great!Thank you!

Last updated: Dec 20 2023 at 11:08 UTC