unused simp argument creative suggestion

Stream: lean4

[Patrick Massot]

A cute little “bug”:

example (a b : Nat) (ha : a = 0) (hb : b = 0) : a + 0 = 0 := by
  simp [hb, ha]

[Patrick Massot]

image.png

[Patrick Massot]

I pasted an image because Zulip messes up the strike-through part.

[Aaron Liu]

well it works

[Joachim Breitner]

It's not a bug, it's a feature! Lean is respectful of your time and the stress on your carpal tunnels, and suggest an edit that takes the least amount of keystrokes to achieve it, including the initial right arrow key presses to get there.

[Joachim Breitner]

But once you are on a version of Lean with https://github.com/leanprover/lean4/pull/8574 it'll stop doing that.