Documentation

Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt

source
def commandDeclare_uint_simprocs_ :
Lean.ParserDescr
Equations
    Instances For
      source
      def UInt8.fromExpr :
      Lean.Expr → Lean.Meta.SimpM (Option UInt8)
      Equations
        Instances For
          source
          def UInt8.reduceLT :
          Lean.Meta.Simp.Simproc
          Equations
            Instances For
              source
              def UInt8.reduceAdd :
              Lean.Meta.Simp.DSimproc
              Equations
                Instances For
                  source
                  def UInt8.reduceToNat :
                  Lean.Meta.Simp.DSimproc
                  Equations
                    Instances For
                      source
                      def UInt8.reduceDiv :
                      Lean.Meta.Simp.DSimproc
                      Equations
                        Instances For
                          source
                          def UInt8.reduceGT :
                          Lean.Meta.Simp.Simproc
                          Equations
                            Instances For
                              source
                              def UInt8.reduceLE :
                              Lean.Meta.Simp.Simproc
                              Equations
                                Instances For
                                  source
                                  def UInt8.reduceMul :
                                  Lean.Meta.Simp.DSimproc
                                  Equations
                                    Instances For
                                      source
                                      def UInt8.reduceMod :
                                      Lean.Meta.Simp.DSimproc
                                      Equations
                                        Instances For
                                          source
                                          def UInt8.reduceGE :
                                          Lean.Meta.Simp.Simproc
                                          Equations
                                            Instances For
                                              source
                                              def UInt8.reduceOfNat :
                                              Lean.Meta.Simp.DSimproc
                                              Equations
                                                Instances For
                                                  source
                                                  def UInt8.reduceSub :
                                                  Lean.Meta.Simp.DSimproc
                                                  Equations
                                                    Instances For
                                                      source
                                                      def UInt8.reduceOfNatLT :
                                                      Lean.Meta.Simp.DSimproc
                                                      Equations
                                                        Instances For
                                                          source
                                                          def UInt16.reduceMod :
                                                          Lean.Meta.Simp.DSimproc
                                                          Equations
                                                            Instances For
                                                              source
                                                              def UInt16.reduceSub :
                                                              Lean.Meta.Simp.DSimproc
                                                              Equations
                                                                Instances For
                                                                  source
                                                                  def UInt16.reduceMul :
                                                                  Lean.Meta.Simp.DSimproc
                                                                  Equations
                                                                    Instances For
                                                                      source
                                                                      def UInt16.reduceToNat :
                                                                      Lean.Meta.Simp.DSimproc
                                                                      Equations
                                                                        Instances For
                                                                          source
                                                                          def UInt16.fromExpr :
                                                                          Lean.Expr → Lean.Meta.SimpM (Option UInt16)
                                                                          Equations
                                                                            Instances For
                                                                              source
                                                                              def UInt16.reduceOfNat :
                                                                              Lean.Meta.Simp.DSimproc
                                                                              Equations
                                                                                Instances For
                                                                                  source
                                                                                  def UInt16.reduceDiv :
                                                                                  Lean.Meta.Simp.DSimproc
                                                                                  Equations
                                                                                    Instances For
                                                                                      source
                                                                                      def UInt16.reduceLT :
                                                                                      Lean.Meta.Simp.Simproc
                                                                                      Equations
                                                                                        Instances For
                                                                                          source
                                                                                          def UInt16.reduceLE :
                                                                                          Lean.Meta.Simp.Simproc
                                                                                          Equations
                                                                                            Instances For
                                                                                              source
                                                                                              def UInt16.reduceAdd :
                                                                                              Lean.Meta.Simp.DSimproc
                                                                                              Equations
                                                                                                Instances For
                                                                                                  source
                                                                                                  def UInt16.reduceGE :
                                                                                                  Lean.Meta.Simp.Simproc
                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      source
                                                                                                      def UInt16.reduceOfNatLT :
                                                                                                      Lean.Meta.Simp.DSimproc
                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          source
                                                                                                          def UInt16.reduceGT :
                                                                                                          Lean.Meta.Simp.Simproc
                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              source
                                                                                                              def UInt32.reduceAdd :
                                                                                                              Lean.Meta.Simp.DSimproc
                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  source
                                                                                                                  def UInt32.reduceOfNat :
                                                                                                                  Lean.Meta.Simp.DSimproc
                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      source
                                                                                                                      def UInt32.reduceDiv :
                                                                                                                      Lean.Meta.Simp.DSimproc
                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          source
                                                                                                                          def UInt32.reduceMul :
                                                                                                                          Lean.Meta.Simp.DSimproc
                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              source
                                                                                                                              def UInt32.reduceGE :
                                                                                                                              Lean.Meta.Simp.Simproc
                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  source
                                                                                                                                  def UInt32.reduceMod :
                                                                                                                                  Lean.Meta.Simp.DSimproc
                                                                                                                                  Equations
                                                                                                                                    Instances For
                                                                                                                                      source
                                                                                                                                      def UInt32.reduceSub :
                                                                                                                                      Lean.Meta.Simp.DSimproc
                                                                                                                                      Equations
                                                                                                                                        Instances For
                                                                                                                                          source
                                                                                                                                          def UInt32.reduceLE :
                                                                                                                                          Lean.Meta.Simp.Simproc
                                                                                                                                          Equations
                                                                                                                                            Instances For
                                                                                                                                              source
                                                                                                                                              def UInt32.reduceOfNatLT :
                                                                                                                                              Lean.Meta.Simp.DSimproc
                                                                                                                                              Equations
                                                                                                                                                Instances For
                                                                                                                                                  source
                                                                                                                                                  def UInt32.fromExpr :
                                                                                                                                                  Lean.Expr → Lean.Meta.SimpM (Option UInt32)
                                                                                                                                                  Equations
                                                                                                                                                    Instances For
                                                                                                                                                      source
                                                                                                                                                      def UInt32.reduceGT :
                                                                                                                                                      Lean.Meta.Simp.Simproc
                                                                                                                                                      Equations
                                                                                                                                                        Instances For
                                                                                                                                                          source
                                                                                                                                                          def UInt32.reduceLT :
                                                                                                                                                          Lean.Meta.Simp.Simproc
                                                                                                                                                          Equations
                                                                                                                                                            Instances For
                                                                                                                                                              source
                                                                                                                                                              def UInt32.reduceToNat :
                                                                                                                                                              Lean.Meta.Simp.DSimproc
                                                                                                                                                              Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  source
                                                                                                                                                                  def UInt64.reduceAdd :
                                                                                                                                                                  Lean.Meta.Simp.DSimproc
                                                                                                                                                                  Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      source
                                                                                                                                                                      def UInt64.reduceMod :
                                                                                                                                                                      Lean.Meta.Simp.DSimproc
                                                                                                                                                                      Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          source
                                                                                                                                                                          def UInt64.reduceGT :
                                                                                                                                                                          Lean.Meta.Simp.Simproc
                                                                                                                                                                          Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              source
                                                                                                                                                                              def UInt64.reduceMul :
                                                                                                                                                                              Lean.Meta.Simp.DSimproc
                                                                                                                                                                              Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  source
                                                                                                                                                                                  def UInt64.reduceGE :
                                                                                                                                                                                  Lean.Meta.Simp.Simproc
                                                                                                                                                                                  Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      source
                                                                                                                                                                                      def UInt64.reduceOfNat :
                                                                                                                                                                                      Lean.Meta.Simp.DSimproc
                                                                                                                                                                                      Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          source
                                                                                                                                                                                          def UInt64.reduceToNat :
                                                                                                                                                                                          Lean.Meta.Simp.DSimproc
                                                                                                                                                                                          Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              source
                                                                                                                                                                                              def UInt64.reduceLT :
                                                                                                                                                                                              Lean.Meta.Simp.Simproc
                                                                                                                                                                                              Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  source
                                                                                                                                                                                                  def UInt64.reduceLE :
                                                                                                                                                                                                  Lean.Meta.Simp.Simproc
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      source
                                                                                                                                                                                                      def UInt64.fromExpr :
                                                                                                                                                                                                      Lean.Expr → Lean.Meta.SimpM (Option UInt64)
                                                                                                                                                                                                      Equations
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          source
                                                                                                                                                                                                          def UInt64.reduceDiv :
                                                                                                                                                                                                          Lean.Meta.Simp.DSimproc
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              source
                                                                                                                                                                                                              def UInt64.reduceOfNatLT :
                                                                                                                                                                                                              Lean.Meta.Simp.DSimproc
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  source
                                                                                                                                                                                                                  def UInt64.reduceSub :
                                                                                                                                                                                                                  Lean.Meta.Simp.DSimproc
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      source
                                                                                                                                                                                                                      def USize.fromExpr (e : Lean.Expr) :
                                                                                                                                                                                                                      Lean.Meta.SimpM (Option USize)
                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          source
                                                                                                                                                                                                                          def USize.reduceToNat :
                                                                                                                                                                                                                          Lean.Meta.Simp.Simproc
                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                            Instances For