Documentation

Lean.Meta.Tactic.Grind.SimpUtil

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

                              Returns the array of simprocs used by grind.

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

                                      Returns the simplification context used by grind.

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