code action "remove tactics after no goals" for "fail"

Stream: general

[Asei Inoue]

import Mathlib.Tactic

example {a b : Int} (h : a = b) : - a ^ 2 + b ^ 2 + (a + b) * (a - b) = 0 := by
  try
    ring
    fail -- Remove tactics after "no goals"

  rw [h]
  ring

[Asei Inoue]

If the above “fail” is removed by code action, the proof will not pass.

[Kyle Miller]

That's amusing.

It makes me wonder if there should be a code action for a try that always fails?

[Asei Inoue]

I feel "remove tactic after no goals" code action is not needed for done or fail

[Asei Inoue]

It makes me wonder if there should be a code action for a try that always fails?

How about all_goals try <tactic>?

[Kyle Miller]

I think the code action would be able to see that there's some evaluation of the try that succeeds