Documentation

Lean.Meta.Tactic.Rewrite

source
structure Lean.Meta.RewriteResult :
Type
Instances For
    source
    def Lean.MVarId.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 }) :
    Lean.MetaM Lean.Meta.RewriteResult

    Rewrite goal mvarId

    Equations
    • One or more equations did not get rendered due to their size.
    source
    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 }) :
    Lean.MetaM Lean.Meta.RewriteResult
    Equations