Documentation

Std.Data.Int.Basic

-[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
    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

      toNat' #

      • If n : Nat, then int.toNat' n = some n
      • If n : Int is negative, then int.toNat' n = none.
      Equations
      Instances For

        Quotient and remainder #

        There are three main conventions for integer division, referred here as the E, F, T rounding conventions. All three pairs satisfy the identity x % y + (x / y) * y = x unconditionally, and satisfy x / 0 = 0 and x % 0 = x.

        E-rounding division #

        This pair satisfies 0 ≤ mod x y < natAbs y for y ≠ 0.

        def Int.ediv :
        IntIntInt

        Integer division. This version of Int.div uses the E-rounding convention (euclidean division), in which Int.emod x y satisfies 0 ≤ mod x y < natAbs y for y ≠ 0 and Int.ediv is the unique function satisfying emod x y + (ediv x y) * y = x.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def Int.emod :
          IntIntInt

          Integer modulus. This version of Int.mod uses the E-rounding convention (euclidean division), in which Int.emod x y satisfies 0 ≤ emod x y < natAbs y for y ≠ 0 and Int.ediv is the unique function satisfying emod x y + (ediv x y) * y = x.

          Equations
          Instances For

            F-rounding division #

            This pair satisfies fdiv x y = floor (x / y).

            def Int.fdiv :
            IntIntInt

            Integer division. This version of Int.div uses the F-rounding convention (flooring division), in which Int.fdiv x y satisfies fdiv x y = floor (x / y) and Int.fmod is the unique function satisfying fmod x y + (fdiv x y) * y = x.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Int.fmod :
              IntIntInt

              Integer modulus. This version of Int.mod uses the F-rounding convention (flooring division), in which Int.fdiv x y satisfies fdiv x y = floor (x / y) and Int.fmod is the unique function satisfying fmod x y + (fdiv x y) * y = x.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                T-rounding division #

                This pair satisfies div x y = round_to_zero (x / y). Int.div and Int.mod are defined in core lean.

                Core Lean provides instances using T-rounding division, i.e. Int.div and Int.mod. We override these here.

                Equations

                gcd #

                def Int.gcd (m : Int) (n : Int) :

                Computes the greatest common divisor of two integers, as a Nat.

                Equations
                Instances For

                  divisibility #

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

                  Equations

                  bit operations #

                  def Int.not :
                  IntInt

                  Bitwise not

                  Interprets the integer as an infinite sequence of bits in two's complement and complements each bit.

                  ~~~(0:Int) = -1
                  ~~~(1:Int) = -2
                  ~~~(-1:Int) = 0
                  
                  Equations
                  Instances For
                    def Int.shiftRight :
                    IntNatInt

                    Bitwise shift right.

                    Conceptually, this treats the integer as an infinite sequence of bits in two's complement and shifts the value to the right.

                    ( 0b0111:Int) >>> 1 =  0b0011
                    ( 0b1000:Int) >>> 1 =  0b0100
                    (-0b1000:Int) >>> 1 = -0b0100
                    (-0b0111:Int) >>> 1 = -0b0100
                    
                    Equations
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.