structure Lean.Meta.RewriteResult : Type

• eNew : Lean.Expr
• eqProof : Lean.Expr
• mvarIds : List Lean.MVarId

def Lean.MVarId.rewrite (mvarId : Lean.MVarId) (e : Lean.Expr) (heq : Lean.Expr) (symm : optParam Bool false) (config : optParam Lean.Meta.Rewrite.Config { transparency := Lean.Meta.TransparencyMode.reducible, offsetCnstrs := true, occs := Lean.Meta.Occurrences.all }) : Lean.MetaM Lean.Meta.RewriteResult

Rewrite goal mvarId

Equations

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

@[deprecated Lean.MVarId.rewrite]

def Lean.Meta.rewrite (mvarId : Lean.MVarId) (e : Lean.Expr) (heq : Lean.Expr) (symm : optParam Bool false) (config : optParam Lean.Meta.Rewrite.Config { transparency := Lean.Meta.TransparencyMode.reducible, offsetCnstrs := true, occs := Lean.Meta.Occurrences.all }) : Lean.MetaM Lean.Meta.RewriteResult

Equations

• Lean.Meta.rewrite mvarId e heq symm config = Lean.MVarId.rewrite mvarId e heq symm config