how do I turn a Term into a rwRule

Stream: lean4

[Scott Morrison]

I want to turn a Term into a TSyntax `Lean.Parser.Tactic.rwRule:

/-- Add a suggestion for `rw [h]`. -/
def addRewriteSuggestion (origTac : Syntax) (e : Expr) (symm : Bool) : TermElabM Unit := do
  let estx ← delabToRefinableSyntax e
  let tac ←
    if symm then
      `(tactic| rw [← $estx])
    else
      `(tactic| rw [$estx]) -- error here: estx has type Term but is expected to have type  TSyntax `Lean.Parser.Tactic.rwRule
  addSuggestion origTac tac

Notice that in the symm branch it works just fine!

[Kyle Miller]

This at least typechecks, but I haven't set up a test to see if it's the right thing: `(tactic| rw [($estx)])

[Kyle Miller]

Ah, right, it's just `(tactic| rw [$estx:term])

[Gabriel Ebner]

And to answer the title of the thread, `(Parser.Tactic.rwRule| $estx:term) .