- eNew : Lean.Expr
- eqProof : Lean.Expr
- mvarIds : List Lean.MVarId
def
Lean.Meta.rewrite
(mvarId : Lean.MVarId)
(e : Lean.Expr)
(heq : Lean.Expr)
(symm : optParam Bool false)
(occs : optParam Lean.Occurrences Lean.Occurrences.all)
(config : optParam Lean.Meta.Rewrite.Config { transparency := Lean.Meta.TransparencyMode.reducible, offsetCnstrs := true })
:
Equations
- One or more equations did not get rendered due to their size.