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) (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

    Instances For
      source
      @[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
      Instances For