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.

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