Documentation

Init.Data.Int.Basic

Integer Type, Coercions, and Notation #

This file defines the Int type as well as

Division and modulus operations are defined in Init.Data.Int.DivMod.Basic.

inductive Int :

The integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The runtime has a special representation for Int that stores “small” signed numbers directly, while larger numbers use a fast arbitrary-precision arithmetic library (usually GMP). A “small number” is an integer that can be encoded with one fewer bits than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit architectures).

  • ofNat : NatInt

    A natural number is an integer.

    This constructor covers the non-negative integers (from 0 to ).

  • negSucc : NatInt

    The negation of the successor of a natural number is an integer.

    This constructor covers the negative integers (from -1 to -∞).

Instances For
    Equations
      instance instOfNat {n : Nat} :
      Equations

        -[n+1] is suggestive notation for negSucc n, which is the second constructor of Int for making strictly negative numbers by mapping n : Nat to -(n + 1).

        Equations
          Instances For

            Coercions #

            @[simp]
            theorem Int.ofNat_eq_coe {n : Nat} :
            ofNat n = n
            @[simp]
            theorem Int.ofNat_zero :
            0 = 0
            @[simp]
            theorem Int.ofNat_one :
            1 = 1
            theorem Int.ofNat_two :
            2 = 2

            Negation of natural numbers.

            Examples:

            Equations
              Instances For
                @[extern lean_int_neg]
                def Int.neg (n : Int) :

                Negation of integers, usually accessed via the - prefix operator.

                This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

                Examples:

                • -(6 : Int) = -6
                • -(-6 : Int) = 6
                • (12 : Int).neg = -12
                Equations
                  Instances For
                    @[defaultInstance 500]
                    Equations
                      def Int.subNatNat (m n : Nat) :

                      Non-truncating subtraction of two natural numbers.

                      Examples:

                      Equations
                        Instances For
                          @[extern lean_int_add]
                          def Int.add (m n : Int) :

                          Addition of integers, usually accessed via the + operator.

                          This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

                          Examples:

                          • (7 : Int) + (6 : Int) = 13
                          • (6 : Int) + (-6 : Int) = 0
                          Equations
                            Instances For
                              instance Int.instAdd :
                              Equations
                                @[extern lean_int_mul]
                                def Int.mul (m n : Int) :

                                Multiplication of integers, usually accessed via the * operator.

                                This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

                                Examples:

                                • (63 : Int) * (6 : Int) = 378
                                • (6 : Int) * (-6 : Int) = -36
                                • (7 : Int) * (0 : Int) = 0
                                Equations
                                  Instances For
                                    instance Int.instMul :
                                    Equations
                                      @[extern lean_int_sub]
                                      def Int.sub (m n : Int) :

                                      Subtraction of integers, usually accessed via the - operator.

                                      This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

                                      Examples:

                                      • (63 : Int) - (6 : Int) = 57
                                      • (7 : Int) - (0 : Int) = 7
                                      • (0 : Int) - (7 : Int) = -7
                                      Equations
                                        Instances For
                                          instance Int.instSub :
                                          Equations
                                            inductive Int.NonNeg :
                                            IntProp

                                            An integer is non-negative if it is equal to a natural number.

                                            Instances For
                                              def Int.le (a b : Int) :

                                              Non-strict inequality of integers, usually accessed via the operator.

                                              a ≤ b is defined as b - a ≥ 0, using Int.NonNeg.

                                              Equations
                                                Instances For
                                                  instance Int.instLEInt :
                                                  Equations
                                                    def Int.lt (a b : Int) :

                                                    Strict inequality of integers, usually accessed via the < operator.

                                                    a < b when a + 1 ≤ b.

                                                    Equations
                                                      Instances For
                                                        instance Int.instLTInt :
                                                        Equations
                                                          @[extern lean_int_dec_eq]
                                                          def Int.decEq (a b : Int) :
                                                          Decidable (a = b)

                                                          Decides whether two integers are equal. Usually accessed via the DecidableEq Int instance.

                                                          This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

                                                          Examples:

                                                          • show (7 : Int) = (3 : Int) + (4 : Int) by decide
                                                          • if (6 : Int) = (3 : Int) * (2 : Int) then "yes" else "no" = "yes"
                                                          • (¬ (6 : Int) = (3 : Int)) = true
                                                          Equations
                                                            Instances For

                                                              Decides whether two integers are equal. Usually accessed via the DecidableEq Int instance.

                                                              This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

                                                              Examples:

                                                              • show (7 : Int) = (3 : Int) + (4 : Int) by decide
                                                              • if (6 : Int) = (3 : Int) * (2 : Int) then "yes" else "no" = "yes"
                                                              • (¬ (6 : Int) = (3 : Int)) = true
                                                              Equations
                                                                @[extern lean_int_dec_le]
                                                                instance Int.decLe (a b : Int) :

                                                                Decides whether a ≤ b.

                                                                #eval ¬ ( (7 : Int) ≤ (0 : Int) ) -- true
                                                                #eval (0 : Int) ≤ (0 : Int) -- true
                                                                #eval (7 : Int) ≤ (10 : Int) -- true
                                                                

                                                                Implemented by efficient native code.

                                                                Equations
                                                                  @[extern lean_int_dec_lt]
                                                                  instance Int.decLt (a b : Int) :
                                                                  Decidable (a < b)

                                                                  Decides whether a < b.

                                                                  #eval `¬ ( (7 : Int) < 0 )` -- true
                                                                  #eval `¬ ( (0 : Int) < 0 )` -- true
                                                                  #eval `(7 : Int) < 10` -- true
                                                                  

                                                                  Implemented by efficient native code.

                                                                  Equations
                                                                    @[extern lean_nat_abs]
                                                                    def Int.natAbs (m : Int) :

                                                                    The absolute value of an integer is its distance from 0.

                                                                    This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

                                                                    Examples:

                                                                    Equations
                                                                      Instances For

                                                                        sign #

                                                                        def Int.sign :
                                                                        IntInt

                                                                        Returns the “sign” of the integer as another integer:

                                                                        • 1 for positive numbers,
                                                                        • -1 for negative numbers, and
                                                                        • 0 for 0.

                                                                        Examples:

                                                                        Equations
                                                                          Instances For

                                                                            Conversion #

                                                                            def Int.toNat :
                                                                            IntNat

                                                                            Converts an integer into a natural number. Negative numbers are converted to 0.

                                                                            Examples:

                                                                            Equations
                                                                              Instances For

                                                                                Converts an integer into a natural number. Returns none for negative numbers.

                                                                                Examples:

                                                                                Equations
                                                                                  Instances For
                                                                                    @[reducible, inline, deprecated Int.toNat? (since := "2025-03-11")]
                                                                                    abbrev Int.toNat' :

                                                                                    Converts an integer into a natural number. Returns none for negative numbers.

                                                                                    Examples:

                                                                                    Equations
                                                                                      Instances For

                                                                                        divisibility #

                                                                                        instance Int.instDvd :

                                                                                        Divisibility of integers. a ∣ b (typed as \|) says that there is some c such that b = a * c.

                                                                                        Equations

                                                                                          Powers #

                                                                                          def Int.pow (m : Int) :
                                                                                          NatInt

                                                                                          Power of an integer to a natural number, usually accessed via the ^ operator.

                                                                                          Examples:

                                                                                          • (2 : Int) ^ 4 = 16
                                                                                          • (10 : Int) ^ 0 = 1
                                                                                          • (0 : Int) ^ 10 = 0
                                                                                          • (-7 : Int) ^ 3 = -343
                                                                                          Equations
                                                                                            Instances For
                                                                                              Equations
                                                                                                instance Int.instMin :
                                                                                                Equations
                                                                                                  instance Int.instMax :
                                                                                                  Equations
                                                                                                    class IntCast (R : Type u) :

                                                                                                    The canonical homomorphism Int → R. In most use cases, the target type will have a ring structure, and this homomorphism should be a ring homomorphism.

                                                                                                    IntCast and NatCast exist to allow different libraries with their own types that can be notated as natural numbers to have consistent simp normal forms without needing to create coercion simplification sets that are aware of all combinations. Libraries should make it easy to work with IntCast where possible. For instance, in Mathlib there will be such a homomorphism (and thus an IntCast R instance) whenever R is an additive group with a 1.

                                                                                                    • intCast : IntR

                                                                                                      The canonical map Int → R.

                                                                                                    Instances
                                                                                                      Equations
                                                                                                        @[reducible, match_pattern]
                                                                                                        def Int.cast {R : Type u} [IntCast R] :
                                                                                                        IntR

                                                                                                        The canonical homomorphism Int → R. In most use cases, the target type will have a ring structure, and this homomorphism should be a ring homomorphism.

                                                                                                        IntCast and NatCast exist to allow different libraries with their own types that can be notated as natural numbers to have consistent simp normal forms without needing to create coercion simplification sets that are aware of all combinations. Libraries should make it easy to work with IntCast where possible. For instance, in Mathlib there will be such a homomorphism (and thus an IntCast R instance) whenever R is an additive group with a 1.

                                                                                                        Equations
                                                                                                          Instances For
                                                                                                            @[simp]
                                                                                                            theorem Int.cast_eq (x : Int) :
                                                                                                            x = x
                                                                                                            instance instCoeTailIntOfIntCast {R : Type u_1} [IntCast R] :
                                                                                                            Equations
                                                                                                              instance instCoeHTCTIntOfIntCast {R : Type u_1} [IntCast R] :
                                                                                                              Equations