Documentation

Mathlib.Init.Data.Int.Bitwise

Lemmas about bitwise operations on integers. #

Possibly only of archaeological significance.

def Int.div2 :

div2 n = n/2

Equations
Instances For
    def Int.bodd :
    Bool

    bodd n returns true if n is odd

    Equations
    Instances For
      def Int.bit (b : Bool) :

      bit b appends the digit b to the binary representation of its integer input.

      Equations
      Instances For
        def Int.testBit :
        Bool

        testBit m n returns whether the (n+1)ˢᵗ least significant bit is 1 or 0

        Equations
        Instances For
          def Int.natBitwise (f : BoolBoolBool) (m : ) (n : ) :

          Int.natBitwise is an auxiliary definition for Int.bitwise.

          Equations
          Instances For
            def Int.bitwise (f : BoolBoolBool) :

            Int.bitwise applies the function f to pairs of bits in the same position in the binary representations of its inputs.

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

              lnot flips all the bits in the binary representation of its input

              Equations
              Instances For
                def Int.lor :

                lor takes two integers and returns their bitwise or

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

                  land takes two integers and returns their bitwise and

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

                    ldiff' a b performs bitwise set difference. For each corresponding pair of bits taken as booleans, say aᵢ and bᵢ, it applies the boolean operation aᵢ ∧ bᵢ to obtain the iᵗʰ bit of the result.

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

                      lxor' computes the bitwise xor of two natural numbers

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

                        m <<< n produces an integer whose binary representation is obtained by left-shifting the binary representation of m by n places

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

                        m >>> n produces an integer whose binary representation is obtained by right-shifting the binary representation of m by n places

                        Equations