def Lean.Elab.Tactic.rewriteTarget (stx : Syntax) (symm : Bool) (config : Meta.Rewrite.Config := { }) : 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 := { }) : 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.
• Lean.Elab.Tactic.withRWRulesSeq.go x symm id declName hint (eqThm :: eqThms) = (x symm (Lean.mkCIdentFrom id eqThm).raw <|> Lean.Elab.Tactic.withRWRulesSeq.go x symm id declName hint eqThms)

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.