Documentation

Lean.Meta.Tactic.Grind.SimpUtil

def Lean.Meta.Grind.registerNormTheorems (preDeclNames postDeclNames : Array Name) :
Equations
    Instances For

      Returns the array of simprocs used by grind.

      Equations
        Instances For

          Returns the simplification context used by grind.

          Equations
            Instances For
              @[export lean_grind_normalize]
              Equations
                Instances For