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

Equations

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

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

def Lean.Elab.Tactic.withRWRulesSeq (token 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 : Lean.Name) (hint : Lean.MessageData) : List Lean.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.Tactic.TacticM Lean.Meta.Rewrite.Config

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