4.27 + apply? + rfl

Stream: lean4

[Julian Berman]

I see leanprover/lean4#11466 so I suspect the answer is "yes that's intended", but just to confirm -- the following trivial examples (from lean.nvim's test suite) both used to produce rfl proofs with old apply?, and now produce slightly more elaborate proof terms. That's intentional in order to avoid checking for this kind of simple proof in other cases, right?

example : 2 = 2 := by apply?
                      └──── Try this:
                              [apply] exact Nat.eq_of_beq_eq_true rfl
example {𝔽 : Type} (x : 𝔽) : x = x := by exact?
                                         └──── Try this:
                                                 [apply] exact ((fun a => a) ∘ fun a => a) rfl

[Kim Morrison]

Yes, this is intentional. Previously, apply? and exact? would first run solve_by_elim directly on the goal, and short-circuit if that succeeded. This was what would produce the rfl proofs.

I decided this was not the appropriate behaviour: these are theorem lookup tools, not general purpose "solve this for me!" tools.

If you would like the old behaviour, I recommend using try?, which calls both solve_by_elim and exact? internally, amongst many other (and user extensible!) things.