Documentation

Init.Data.Int.Basic

Integer Type, Coercions, and Notation #

This file defines the Int type as well as

inductive Int :
  • 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 -∞).

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).

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

    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
            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
              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
              Instances For
                Equations
                inductive Int.NonNeg :
                IntProp

                A proof that an Int is non-negative.

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

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

                  Equations
                  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
                          @[extern lean_int_div]
                          def Int.div :
                          IntIntInt

                          Integer division. This function uses the "T-rounding" (Truncation-rounding) convention, meaning that it rounds toward zero. Also note that division by zero is defined to equal zero.

                          The relation between integer division and modulo is found in the Int.mod_add_div theorem in std which states that a % b + b * (a / b) = a, unconditionally.

                          Examples:

                          #eval (7 : Int) / (0 : Int) -- 0
                          #eval (0 : Int) / (7 : Int) -- 0
                          
                          #eval (12 : Int) / (6 : Int) -- 2
                          #eval (12 : Int) / (-6 : Int) -- -2
                          #eval (-12 : Int) / (6 : Int) -- -2
                          #eval (-12 : Int) / (-6 : Int) -- 2
                          
                          #eval (12 : Int) / (7 : Int) -- 1
                          #eval (12 : Int) / (-7 : Int) -- -1
                          #eval (-12 : Int) / (7 : Int) -- -1
                          #eval (-12 : Int) / (-7 : Int) -- 1
                          

                          Implemented by efficient native code.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            @[extern lean_int_mod]
                            def Int.mod :
                            IntIntInt

                            Integer modulo. This function uses the "T-rounding" (Truncation-rounding) convention to pair with Int.div, meaning that a % b + b * (a / b) = a unconditionally (see Int.mod_add_div). In particular, a % 0 = a.

                            Examples:

                            #eval (7 : Int) % (0 : Int) -- 7
                            #eval (0 : Int) % (7 : Int) -- 0
                            
                            #eval (12 : Int) % (6 : Int) -- 0
                            #eval (12 : Int) % (-6 : Int) -- 0
                            #eval (-12 : Int) % (6 : Int) -- 0
                            #eval (-12 : Int) % (-6 : Int) -- 0
                            
                            #eval (12 : Int) % (7 : Int) -- 5
                            #eval (12 : Int) % (-7 : Int) -- 5
                            #eval (-12 : Int) % (7 : Int) -- 2
                            #eval (-12 : Int) % (-7 : Int) -- 2
                            

                            Implemented by efficient native code.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              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
                                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
                                Instances For
                                  Equations
                                  Equations