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

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.