def Lean.Elab.Tactic.rewriteTarget (stx : Lean.Syntax) (symm : Bool) (config : optParam Lean.Meta.Rewrite.Config { transparency := Lean.Meta.TransparencyMode.reducible, offsetCnstrs := true, occs := Lean.Meta.Occurrences.all }) : Lean.Elab.Tactic.TacticM Unit

def Lean.Elab.Tactic.rewriteLocalDecl (stx : Lean.Syntax) (symm : Bool) (fvarId : Lean.FVarId) (config : optParam Lean.Meta.Rewrite.Config { transparency := Lean.Meta.TransparencyMode.reducible, offsetCnstrs := true, occs := Lean.Meta.Occurrences.all }) : Lean.Elab.Tactic.TacticM Unit

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

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

Equations

• One or more equations did not get rendered due to their size.

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

def Lean.Elab.Tactic.evalRewriteSeq : Lean.Elab.Tactic.Tactic