Documentation

Lean.Meta.Tactic.Rewrite

Instances For
    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.
    Instances For