def Lean.Elab.Tactic.rewriteTarget (stx : Syntax) (symm : Bool) (config : Meta.Rewrite.Config := { }) : TacticM Unit

def Lean.Elab.Tactic.rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Meta.Rewrite.Config := { }) : TacticM Unit

def Lean.Elab.Tactic.withRWRulesSeq (token rwRulesSeqStx : Syntax) (x : Bool → Syntax → TacticM Unit) : TacticM Unit

def Lean.Elab.Tactic.withRWRulesSeq.go (x : Bool → Syntax → TacticM Unit) (symm : Bool) (id : Syntax) (declName : Name) (hint : MessageData) : List Name → TacticM Unit

def Lean.Elab.Tactic.elabRewriteConfig : Syntax → TacticM Meta.Rewrite.Config

def Lean.Elab.Tactic.evalRewriteSeq : Tactic