source
structure Lean.Meta.RewriteResult :
Type

- eNew : Expr
- eqProof : Expr
- mvarIds : List MVarId

Instances For

source
def Lean.MVarId.rewrite (mvarId : MVarId) (e heq : Expr) (symm : Bool := false) (config : Meta.Rewrite.Config := { }) :
MetaM Meta.RewriteResult

Rewrite `e` using `heq` in the context of `mvarId`. Returns the result of the rewrite, the metavariable `mvarId` is not assigned.

Equations

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

Instances For