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.
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