def Lean.Elab.Tactic.elabRewrite (mvarId : MVarId) (e : Expr) (stx : Syntax) (symm : Bool := false) (config : Meta.Rewrite.Config := { }) : TacticM Meta.RewriteResult

Runs Lean.MVarId.rewrite, and also handles filtering out the old metavariables in the rewrite result. This should be used from within withSynthesize. Use finishElabRewrite once elaboration is complete to make final updates to RewriteResult.

Equations

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

def Lean.Elab.Tactic.finishElabRewrite (r : Meta.RewriteResult) : MetaM Meta.RewriteResult

Makes new goals be synthetic opaque, to be done once elaboration of the rewrite theorem is complete.

Workaround note: we are only doing this for proof goals, not data goals, since there are many downstream cases of tactic proofs that later assign data goals by unification.

Equations

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

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.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.