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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Tactic.evalRewriteSeq : Tactic

Equations

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