Helper functions for debugging purposes and creating tests.

def Lean.Meta.Sym.mkSimprocFor (declNames : Array Name) (d : Simp.Discharger := Simp.dischargeNone) : MetaM Simp.Simproc

Equations

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

def Lean.Meta.Sym.mkMethods (declNames : Array Name) : MetaM Simp.Methods

Equations

• Lean.Meta.Sym.mkMethods declNames = do let __do_lift ← Lean.Meta.Sym.mkSimprocFor declNames pure { post := __do_lift }

def Lean.Meta.Sym.simpGoalUsing (declNames : Array Name) (mvarId : MVarId) : MetaM (Option MVarId)

Equations

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