How to use let rec in proofs?

Stream: new members

[Jiatong Yang]

(Lean4)
It seems that if using let rec like this, the new definition will not appear in the context.

import Mathlib

theorem t0 : True := by
  let rec f : ℕ → ℕ
  | 0 => 0
  | 1 => 1
  | n + 2 => f n + f (n + 1)
  have h : f 0 = 0 := rfl

[Aaron Liu]

Kyle Miller said:

It's because let rec defers creating the auxiliary definitions until everything is elaborated. It's a limitation that I don't expect to see change.