Documentation

Lean.Meta.Tactic.Grind.SimpUtil

source
def Lean.Meta.Grind.registerNormTheorems (preDeclNames postDeclNames : Array Name) :
MetaM Unit
Instances For
    source
    def Lean.Meta.Grind.simpEq :
    Simp.Simproc
    Instances For
      source
      def Lean.Meta.Grind.simpDIte :
      Simp.Simproc
      Instances For
        source
        def Lean.Meta.Grind.pushNot :
        Simp.Simproc
        Instances For
          source
          def Lean.Meta.Grind.simpOr :
          Simp.Simproc
          Instances For
            source
            def Lean.Meta.Grind.reduceCtorEqCheap :
            Simp.Simproc
            Instances For
              source
              def Lean.Meta.Grind.unfoldReducibleSimproc :
              Simp.DSimproc
              Instances For
                source
                def Lean.Meta.Grind.getSimprocs :
                MetaM (Array Simprocs)

                Returns the array of simprocs used by grind.

                Instances For
                  source
                  def Lean.Meta.Grind.getNormTheorems :
                  MetaM SimpTheorems
                  Instances For
                    source
                    def Lean.Meta.Grind.getSimpContext (config : Grind.Config) :
                    MetaM Simp.Context

                    Returns the simplification context used by grind.

                    Instances For
                      source
                      @[export lean_grind_normalize]
                      def Lean.Meta.Grind.normalizeImp (e : Expr) (config : Grind.Config) :
                      MetaM Expr
                      Instances For