listing config options of a tactic

Stream: new members

[Lawrence Wu (llllvvuu)]

is there a general way to list the config options of a tactic? the only way i'm aware is to go to the mathlib docs and search for <TacticName>.Config, e.g. docs#Lean.Try.Config, docs#Lean.Grind.Config, docs#Lean.Meta.Simp.Config

Like an equivalent of --help or something? Hover doesn't work, and go-to-def goes to something like

@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do withSimpDiagnostics do
  let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
  let stats ← dischargeWrapper.with fun discharge? =>
    simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
  if tactic.simp.trace.get (← getOptions) then
    traceSimpCall stx stats.usedTheorems
  return stats.diag

and now I'm lost

[Robin Arnez]

You can use simp (config := { <cursor> }) and then trigger autocompletion