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.rewriteLocalDeclCore (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Meta.Rewrite.Config := { }) : TacticM FVarId

Rewrites a local declaration and returns the replacement free variable.

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

• Lean.Elab.Tactic.rewriteLocalDecl stx symm fvarId config = discard (Lean.Elab.Tactic.rewriteLocalDeclCore stx symm fvarId config)

def Lean.Elab.Tactic.foldRWRulesSeq {α : Type} (token rwRulesSeqStx : Syntax) (init : α) (x : α → Bool → Syntax → TacticM α) : TacticM α

Folds a tactic action over a sequence of rewrite rules.

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

• Lean.Elab.Tactic.withRWRulesSeq token rwRulesSeqStx x = discard (Lean.Elab.Tactic.foldRWRulesSeq token rwRulesSeqStx () fun (x_1 : Unit) (symm : Bool) (term : Lean.Syntax) => x symm term)

def Lean.Elab.Tactic.elabRewriteConfig (cfg : Syntax) (init : Meta.Rewrite.Config := { }) (logExceptions : Bool := true) : 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.