I'm starting to learn about Lean programming language https://leanprover.github.io

I've found out that there are functions, structures, if/else, and other common programming commands.

However, I haven't found anything to deal with loops. Is there a way of iterating or repeating a block of code in Lean? Something similar to for or while in other languages. If so, please add the syntaxis or an example.

Thank you in advance.

CodePudding user response：

Like other functional programming languages, loops in Lean are primarily done via recursion. For example:

-- lean 3
def numbers : ℕ → list ℕ
| 0 := []
| (n 1) := n :: numbers n

This is a bit of a change of mindset if you aren't used to it. See: Haskell from C: Where are the for Loops?

To complicate matters, Lean makes a distinction between general recursion and structural recursion. The above example is using structural recursion on ℕ, so we know that it always halts. Non-halting programs can lead to inconsistency in a DTT-based theorem prover like lean, so it has to be strictly controlled. You can opt in to general recursion using the meta keyword:

-- lean 3
meta def foo : ℕ → ℕ
| n := if n = 100 then 0 else foo (n   1)   1

In lean 4, the do block syntax includes a for command, which can be used to write for loops in a more imperative style. Note that they are still represented as tail-recursive functions under the hood, and there are some typeclasses powering the desugaring. (Also you need the partial keyword instead of meta to do general recursion in lean 4.)

-- lean 4
partial def foo (n : Nat) : Nat :=
  if n = 100 then 0 else foo (n   1)   1

def mySum (n : Nat) : Nat := Id.run do
  let mut acc := 0
  for i in [0:n] do
    acc := acc   i
  pure acc