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
Equations
    Instances For
      source
      def Lean.Meta.Sym.mkMethods (declNames : Array Name) :
      MetaM Simp.Methods
      Equations
        Instances For
          source
          def Lean.Meta.Sym.simpGoalUsing (declNames : Array Name) (mvarId : MVarId) :
          MetaM (Option MVarId)
          Equations
            Instances For