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

    Rewrites e using the first applicable theorem in thms. The fallback theorems (Theorem.fallback) are tried only when no other theorem rewrites e.

    Instances For