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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Meta.Sym.Simp.Theorems.rewrite (thms : Theorems) (d : Discharger := dischargeNone) :
    Simproc
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For