simp? does not work in conv mode

[MichaelStollBayreuth]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Trying to use simp? in conv mode gives an error "unexpected identifier; expected command".

Context

simp and simp only are valid tactics in conv mode. So it would be natural if simp? would also work (and allow to replace simp calls by simp only calls for efficiency).

See the discussion on Zulip.

Steps to Reproduce

MWE:

example (n : Nat) : 123 + 2 * n = 123 + (n + n) := by
  conv =>
    enter [1, 2]
    simp? -- error

Expected behavior:

simp? should work in conv mode in the same way as it does normally.

Actual behavior:

simp? in conv mode results in an error.

Versions

Lean 4.15.0-nightly-2024-11-21
Target: x86_64-unknown-linux-gnu

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[kim-em]

I think this would not be too hard to implement. If anyone would like to submit a PR we would surely review it!