def
Lean.MVarId.rewrite
(mvarId : MVarId)
(e heq : Expr)
(symm : Bool := false)
(config : Meta.Rewrite.Config := { })
:
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.