Documentation

Lean.Meta.Sym.Simp.Rewrite

source
def Lean.Meta.Sym.Simp.Theorem.rewrite (thm : Theorem) (e : Expr) (d : Discharger := dischargeNone) :
SimpM Result

Tries to rewrite e using the given theorem.

Equations
    Instances For
      source
      def Lean.Meta.Sym.Simp.Theorems.rewrite (thms : Theorems) (d : Discharger := dischargeNone) :
      Simproc
      Equations
        Instances For