Documentation

Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt

source
def commandDeclare_sint_simprocs_ :
Lean.ParserDescr
Equations
    Instances For
      source
      def Int8.reduceOfNat :
      Lean.Meta.Simp.DSimproc
      Equations
        Instances For
          source
          def Int8.reduceLT :
          Lean.Meta.Simp.Simproc
          Equations
            Instances For
              source
              def Int8.reduceMod :
              Lean.Meta.Simp.DSimproc
              Equations
                Instances For
                  source
                  def Int8.reduceSub :
                  Lean.Meta.Simp.DSimproc
                  Equations
                    Instances For
                      source
                      def Int8.reduceAdd :
                      Lean.Meta.Simp.DSimproc
                      Equations
                        Instances For
                          source
                          def Int8.reduceLE :
                          Lean.Meta.Simp.Simproc
                          Equations
                            Instances For
                              source
                              def Int8.reduceOfInt :
                              Lean.Meta.Simp.DSimproc
                              Equations
                                Instances For
                                  source
                                  def Int8.reduceToInt :
                                  Lean.Meta.Simp.DSimproc
                                  Equations
                                    Instances For
                                      source
                                      def Int8.fromExpr :
                                      Lean.Expr → Lean.Meta.SimpM (Option Int8)
                                      Equations
                                        Instances For
                                          source
                                          def Int8.reduceGT :
                                          Lean.Meta.Simp.Simproc
                                          Equations
                                            Instances For
                                              source
                                              def Int8.reduceDiv :
                                              Lean.Meta.Simp.DSimproc
                                              Equations
                                                Instances For
                                                  source
                                                  def Int8.reduceOfIntLE :
                                                  Lean.Meta.Simp.DSimproc
                                                  Equations
                                                    Instances For
                                                      source
                                                      def Int8.reduceMul :
                                                      Lean.Meta.Simp.DSimproc
                                                      Equations
                                                        Instances For
                                                          source
                                                          def Int8.reduceToNatClampNeg :
                                                          Lean.Meta.Simp.DSimproc
                                                          Equations
                                                            Instances For
                                                              source
                                                              def Int8.reduceGE :
                                                              Lean.Meta.Simp.Simproc
                                                              Equations
                                                                Instances For
                                                                  source
                                                                  def Int16.reduceDiv :
                                                                  Lean.Meta.Simp.DSimproc
                                                                  Equations
                                                                    Instances For
                                                                      source
                                                                      def Int16.reduceLT :
                                                                      Lean.Meta.Simp.Simproc
                                                                      Equations
                                                                        Instances For
                                                                          source
                                                                          def Int16.reduceLE :
                                                                          Lean.Meta.Simp.Simproc
                                                                          Equations
                                                                            Instances For
                                                                              source
                                                                              def Int16.reduceSub :
                                                                              Lean.Meta.Simp.DSimproc
                                                                              Equations
                                                                                Instances For
                                                                                  source
                                                                                  def Int16.reduceGT :
                                                                                  Lean.Meta.Simp.Simproc
                                                                                  Equations
                                                                                    Instances For
                                                                                      source
                                                                                      def Int16.fromExpr :
                                                                                      Lean.Expr → Lean.Meta.SimpM (Option Int16)
                                                                                      Equations
                                                                                        Instances For
                                                                                          source
                                                                                          def Int16.reduceGE :
                                                                                          Lean.Meta.Simp.Simproc
                                                                                          Equations
                                                                                            Instances For
                                                                                              source
                                                                                              def Int16.reduceToNatClampNeg :
                                                                                              Lean.Meta.Simp.DSimproc
                                                                                              Equations
                                                                                                Instances For
                                                                                                  source
                                                                                                  def Int16.reduceAdd :
                                                                                                  Lean.Meta.Simp.DSimproc
                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      source
                                                                                                      def Int16.reduceToInt :
                                                                                                      Lean.Meta.Simp.DSimproc
                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          source
                                                                                                          def Int16.reduceOfIntLE :
                                                                                                          Lean.Meta.Simp.DSimproc
                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              source
                                                                                                              def Int16.reduceMul :
                                                                                                              Lean.Meta.Simp.DSimproc
                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  source
                                                                                                                  def Int16.reduceOfNat :
                                                                                                                  Lean.Meta.Simp.DSimproc
                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      source
                                                                                                                      def Int16.reduceOfInt :
                                                                                                                      Lean.Meta.Simp.DSimproc
                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          source
                                                                                                                          def Int16.reduceMod :
                                                                                                                          Lean.Meta.Simp.DSimproc
                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              source
                                                                                                                              def Int32.reduceLE :
                                                                                                                              Lean.Meta.Simp.Simproc
                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  source
                                                                                                                                  def Int32.reduceToNatClampNeg :
                                                                                                                                  Lean.Meta.Simp.DSimproc
                                                                                                                                  Equations
                                                                                                                                    Instances For
                                                                                                                                      source
                                                                                                                                      def Int32.reduceOfNat :
                                                                                                                                      Lean.Meta.Simp.DSimproc
                                                                                                                                      Equations
                                                                                                                                        Instances For
                                                                                                                                          source
                                                                                                                                          def Int32.reduceSub :
                                                                                                                                          Lean.Meta.Simp.DSimproc
                                                                                                                                          Equations
                                                                                                                                            Instances For
                                                                                                                                              source
                                                                                                                                              def Int32.reduceOfIntLE :
                                                                                                                                              Lean.Meta.Simp.DSimproc
                                                                                                                                              Equations
                                                                                                                                                Instances For
                                                                                                                                                  source
                                                                                                                                                  def Int32.reduceDiv :
                                                                                                                                                  Lean.Meta.Simp.DSimproc
                                                                                                                                                  Equations
                                                                                                                                                    Instances For
                                                                                                                                                      source
                                                                                                                                                      def Int32.reduceGE :
                                                                                                                                                      Lean.Meta.Simp.Simproc
                                                                                                                                                      Equations
                                                                                                                                                        Instances For
                                                                                                                                                          source
                                                                                                                                                          def Int32.reduceGT :
                                                                                                                                                          Lean.Meta.Simp.Simproc
                                                                                                                                                          Equations
                                                                                                                                                            Instances For
                                                                                                                                                              source
                                                                                                                                                              def Int32.fromExpr :
                                                                                                                                                              Lean.Expr → Lean.Meta.SimpM (Option Int32)
                                                                                                                                                              Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  source
                                                                                                                                                                  def Int32.reduceOfInt :
                                                                                                                                                                  Lean.Meta.Simp.DSimproc
                                                                                                                                                                  Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      source
                                                                                                                                                                      def Int32.reduceLT :
                                                                                                                                                                      Lean.Meta.Simp.Simproc
                                                                                                                                                                      Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          source
                                                                                                                                                                          def Int32.reduceAdd :
                                                                                                                                                                          Lean.Meta.Simp.DSimproc
                                                                                                                                                                          Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              source
                                                                                                                                                                              def Int32.reduceToInt :
                                                                                                                                                                              Lean.Meta.Simp.DSimproc
                                                                                                                                                                              Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  source
                                                                                                                                                                                  def Int32.reduceMul :
                                                                                                                                                                                  Lean.Meta.Simp.DSimproc
                                                                                                                                                                                  Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      source
                                                                                                                                                                                      def Int32.reduceMod :
                                                                                                                                                                                      Lean.Meta.Simp.DSimproc
                                                                                                                                                                                      Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          source
                                                                                                                                                                                          def Int64.reduceDiv :
                                                                                                                                                                                          Lean.Meta.Simp.DSimproc
                                                                                                                                                                                          Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              source
                                                                                                                                                                                              def Int64.reduceGT :
                                                                                                                                                                                              Lean.Meta.Simp.Simproc
                                                                                                                                                                                              Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  source
                                                                                                                                                                                                  def Int64.reduceMul :
                                                                                                                                                                                                  Lean.Meta.Simp.DSimproc
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      source
                                                                                                                                                                                                      def Int64.reduceToNatClampNeg :
                                                                                                                                                                                                      Lean.Meta.Simp.DSimproc
                                                                                                                                                                                                      Equations
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          source
                                                                                                                                                                                                          def Int64.reduceOfIntLE :
                                                                                                                                                                                                          Lean.Meta.Simp.DSimproc
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              source
                                                                                                                                                                                                              def Int64.reduceOfNat :
                                                                                                                                                                                                              Lean.Meta.Simp.DSimproc
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  source
                                                                                                                                                                                                                  def Int64.reduceToInt :
                                                                                                                                                                                                                  Lean.Meta.Simp.DSimproc
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      source
                                                                                                                                                                                                                      def Int64.reduceLE :
                                                                                                                                                                                                                      Lean.Meta.Simp.Simproc
                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          source
                                                                                                                                                                                                                          def Int64.fromExpr :
                                                                                                                                                                                                                          Lean.Expr → Lean.Meta.SimpM (Option Int64)
                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              source
                                                                                                                                                                                                                              def Int64.reduceGE :
                                                                                                                                                                                                                              Lean.Meta.Simp.Simproc
                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  source
                                                                                                                                                                                                                                  def Int64.reduceAdd :
                                                                                                                                                                                                                                  Lean.Meta.Simp.DSimproc
                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                      source
                                                                                                                                                                                                                                      def Int64.reduceLT :
                                                                                                                                                                                                                                      Lean.Meta.Simp.Simproc
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                          source
                                                                                                                                                                                                                                          def Int64.reduceOfInt :
                                                                                                                                                                                                                                          Lean.Meta.Simp.DSimproc
                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                              source
                                                                                                                                                                                                                                              def Int64.reduceMod :
                                                                                                                                                                                                                                              Lean.Meta.Simp.DSimproc
                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                  source
                                                                                                                                                                                                                                                  def Int64.reduceSub :
                                                                                                                                                                                                                                                  Lean.Meta.Simp.DSimproc
                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                      source
                                                                                                                                                                                                                                                      def ISize.reduceToNatClampNeg :
                                                                                                                                                                                                                                                      Lean.Meta.Simp.Simproc
                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                          source
                                                                                                                                                                                                                                                          def ISize.reduceToInt :
                                                                                                                                                                                                                                                          Lean.Meta.Simp.Simproc
                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                            Instances For