Failing example in chapter Inductive Types

[whxvd]

On my end, the example

open Nat
theorem add_assoc (m n k : Nat) : m + n + k = m + (n + k) :=
  Nat.recOn (motive := fun k => m + n + k = m + (n + k)) k
    rfl
    (fun k ih => by simp [Nat.add_succ, ih])

from https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html fails with:

tactic 'simp' failed, nested error:
maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information

I am still new to Lean. I installed a Lean toolchain with elan from the AUR package elan-lean on Arch Linux some weeks ago. Then I somehow create a test repository with lake. After stumbling upon this issue, I ran lake update and elan update. Now elan show outputs

installed toolchains
--------------------

leanprover/lean4:stable
leanprover/lean4:v4.10.0-rc2

active toolchain
----------------

leanprover/lean4:stable (overridden by '/home/w/line/lean/lean-toolchain')
Lean (version 4.11.0, x86_64-unknown-linux-gnu, commit ec3042d94bd1, Release)

when I am in the test repository where I play with and learn Lean. I do not yet know any details about elan, lake, and the whole build system. But I suppose, that I am up-to-date.

[whxvd]

Sorry, wrong repository. In the correct repository, this already is reported, see leanprover/theorem_proving_in_lean4#120.