Documentation

Init.Data.Int.Basic

Integer Type, Coercions, and Notation #

This file defines the Int type as well as

inductive Int :

The type of integers. It is defined as an inductive type based on the natural number type Nat featuring two constructors: "a natural number is an integer", and "the negation of a successor of a natural number is an integer". The former represents integers between 0 (inclusive) and , and the latter integers between -∞ and -1 (inclusive).

This type is special-cased by the compiler. The runtime has a special representation for Int which stores "small" signed numbers directly, and larger numbers use an arbitrary precision "bignum" library (usually GMP). A "small number" is an integer that can be encoded with 63 bits (31 bits on 32-bits architectures).

  • ofNat: NatInt

    A natural number is an integer (0 to ).

  • negSucc: NatInt

    The negation of the successor of a natural number is an integer (-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
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem Int.default_eq_zero :
      default = 0

      Coercions #

      @[simp]
      theorem Int.ofNat_eq_coe {n : Nat} :
      Int.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 a natural number.

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

        Negation of an integer.

        Implemented by efficient native code.

        Equations
        Instances For
          @[defaultInstance 500]
          Equations
          def Int.subNatNat (m : Nat) (n : Nat) :

          Subtraction of two natural numbers.

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

            Addition of two integers.

            #eval (7 : Int) + (6 : Int) -- 13
            #eval (6 : Int) + (-6 : Int) -- 0
            

            Implemented by efficient native code.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              instance Int.instAdd :
              Equations
              @[extern lean_int_mul]
              def Int.mul (m : Int) (n : Int) :

              Multiplication of two integers.

              #eval (63 : Int) * (6 : Int) -- 378
              #eval (6 : Int) * (-6 : Int) -- -36
              #eval (7 : Int) * (0 : Int) -- 0
              

              Implemented by efficient native code.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                instance Int.instMul :
                Equations
                @[extern lean_int_sub]
                def Int.sub (m : Int) (n : Int) :

                Subtraction of two integers.

                #eval (63 : Int) - (6 : Int) -- 57
                #eval (7 : Int) - (0 : Int) -- 7
                #eval (0 : Int) - (7 : Int) -- -7
                

                Implemented by efficient native code.

                Equations
                • m.sub n = m + -n
                Instances For
                  instance Int.instSub :
                  Equations
                  inductive Int.NonNeg :
                  IntProp

                  A proof that an Int is non-negative.

                  • mk: ∀ (n : Nat), (Int.ofNat n).NonNeg

                    Sole constructor, proving that ofNat n is positive.

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

                    Definition of a ≤ b, encoded as b - a ≥ 0.

                    Equations
                    • a.le b = (b - a).NonNeg
                    Instances For
                      instance Int.instLEInt :
                      Equations
                      def Int.lt (a : Int) (b : Int) :

                      Definition of a < b, encoded as a + 1 ≤ b.

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

                        Decides equality between two Ints.

                        #eval (7 : Int) = (3 : Int) + (4 : Int) -- true
                        #eval (6 : Int) = (3 : Int) * (2 : Int) -- true
                        #eval ¬ (6 : Int) = (3 : Int) -- true
                        

                        Implemented by efficient native code.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[extern lean_int_dec_le]
                          instance Int.decLe (a : Int) (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 : Int) (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) :

                          Absolute value (Nat) of an integer.

                          #eval (7 : Int).natAbs -- 7
                          #eval (0 : Int).natAbs -- 0
                          #eval (-11 : Int).natAbs -- 11
                          

                          Implemented by efficient native code.

                          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.

                            Equations
                            Instances For

                              Conversion #

                              def Int.toNat :
                              IntNat

                              Turns an integer into a natural number, negative numbers become 0.

                              #eval (7 : Int).toNat -- 7
                              #eval (0 : Int).toNat -- 0
                              #eval (-7 : Int).toNat -- 0
                              
                              Equations
                              Instances For
                                • If n : Nat, then int.toNat' n = some n
                                • If n : Int is negative, then int.toNat' n = none.
                                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 some natural number.

                                  #eval (2 : Int) ^ 4 -- 16
                                  #eval (10 : Int) ^ 0 -- 1
                                  #eval (0 : Int) ^ 10 -- 0
                                  #eval (-7 : Int) ^ 3 -- -343
                                  
                                  Equations
                                  • m.pow 0 = 1
                                  • m.pow m_1.succ = m.pow m_1 * m
                                  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 R will have a ring structure and this will be a ring homomorphism.

                                    • intCast : IntR

                                      The canonical map Int → R.

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

                                      Apply the canonical homomorphism from Int to a type R from an IntCast R instance.

                                      In Mathlib there will be such a homomorphism whenever R is an additive group with a 1.

                                      Equations
                                      • Int.cast = IntCast.intCast
                                      Instances For
                                        instance instCoeTailIntOfIntCast {R : Type u_1} [IntCast R] :
                                        Equations
                                        • instCoeTailIntOfIntCast = { coe := Int.cast }
                                        instance instCoeHTCTIntOfIntCast {R : Type u_1} [IntCast R] :
                                        Equations
                                        • instCoeHTCTIntOfIntCast = { coe := Int.cast }