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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

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

Instances For

source
def Lean.Elab.Tactic.evalRewriteSeq :
Tactic
Equations

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

Instances For