by apply?

Stream: lean4

[Patrick Massot]

Am I dreaming or did Lean 3 had the nice feature that by apply? was replaced by a proof term when it closed the goal (ie foo bar instead of by exact foo bar)? Anyway, it would be really nice to have.

[Floris van Doorn]

Is this close enough to what you want?

example : True := exact?%

[Floris van Doorn]

But you're correct that at some point clicking on by exact? would give you something that never went into tactic mode.

[Patrick Massot]

I know about exact?% but I still think getting back that behavior would be really nice.

[Mario Carneiro]

this can be a general try this behavior - whenever the replacement is exact foo and it's alone in it's by block you can delete both by and exact

[Eric Wieser]

That's not always true, sometimes by exact is needed to adjust the elaboration order

[Ruben Van de Velde]

But close enough for cases like exact?, I think