let rec expression must be named with induction on field

Stream: lean4

[Jakub Nowak]

I think that worked before, but maybe not?

structure Foo where
  n : Nat

/-- error: 'let rec' expressions must be named -/
#guard_msgs in
example (foo : Foo) := by
  induction foo.n where
  | zero => sorry
  | succ n => sorry

[Jakub Nowak]

Oh, wait, it should be with, not where...
We should definitely fix that error message.

[Kevin Buzzard]

Slightly tangential but there's a code action which writes the correct syntax for you:

Screenshot from 2025-12-22 19-29-55.png

[Jakub Nowak]

Hm, there's something weird with it though. It doesn't work on https://live.lean-lang.org nor in neovim.

[Jakub Nowak]

I've just checked and it also doesn't work for me in vscode. Is this feature from nightly?

[Jakub Nowak]

Ahh, you need import Mathlib import Batteries for it to work.