Documentation

Lean.Meta.Tactic.Grind.SimpUtil

source
opaque Lean.Meta.Grind.normExt :
SimpExtension
source
def Lean.Meta.Grind.registerNormTheorems (preDeclNames postDeclNames : Array Name) :
MetaM Unit
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Meta.Grind.simpBoolEq :
    Simp.Simproc
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Meta.Grind.getSimprocs :
      MetaM (Array Simprocs)

      Returns the array of simprocs used by grind.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Meta.Grind.getSimpContext (config : Grind.Config) :
        MetaM Simp.Context

        Returns the simplification context used by grind.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[export lean_grind_normalize]
          def Lean.Meta.Grind.normalizeImp (e : Expr) (config : Grind.Config) :
          MetaM Expr
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For