Documentation

Lean.Meta.Sym.Simp.Debug

Helper functions for debugging purposes and creating tests.

source
def Lean.Meta.Sym.mkSimprocFor (declNames : Array Name) (d : Simp.Discharger := Simp.dischargeNone) :
MetaM Simp.Simproc
Instances For
    source
    def Lean.Meta.Sym.mkMethods (declNames : Array Name) :
    MetaM Simp.Methods
    Instances For
      source
      def Lean.Meta.Sym.simpGoalUsing (declNames : Array Name) (mvarId : MVarId) :
      MetaM (Option MVarId)
      Instances For