Documentation

Init.Data.Nat.Bitwise.Basic

theorem Nat.bitwise_rec_lemma {n : Nat} (hNe : n 0) :
n / 2 < n
@[irreducible]
def Nat.bitwise (f : BoolBoolBool) (n m : Nat) :

A helper for implementing bitwise operators on Nat.

Each bit of the resulting Nat is the result of applying f to the corresponding bits of the input Nats, up to the position of the highest set bit in either input.

Equations
    Instances For
      @[extern lean_nat_land]
      def Nat.land :
      NatNatNat

      Bitwise and. Usually accessed via the &&& operator.

      Each bit of the resulting value is set if the corresponding bit is set in both of the inputs.

      Equations
        Instances For
          @[extern lean_nat_lor]
          def Nat.lor :
          NatNatNat

          Bitwise or. Usually accessed via the ||| operator.

          Each bit of the resulting value is set if the corresponding bit is set in at least one of the inputs.

          Equations
            Instances For
              @[extern lean_nat_lxor]
              def Nat.xor :
              NatNatNat

              Bitwise exclusive or. Usually accessed via the ^^^ operator.

              Each bit of the resulting value is set if the corresponding bit is set in exactly one of the inputs.

              Equations
                Instances For
                  @[extern lean_nat_shiftl]
                  def Nat.shiftLeft :
                  NatNatNat

                  Shifts the binary representation of a value left by the specified number of bits. Usually accessed via the <<< operator.

                  Examples:

                  • 1 <<< 2 = 4
                  • 1 <<< 3 = 8
                  • 0 <<< 3 = 0
                  • 0xf1 <<< 4 = 0xf10
                  Equations
                    Instances For
                      @[extern lean_nat_shiftr]
                      def Nat.shiftRight :
                      NatNatNat

                      Shifts the binary representation of a value right by the specified number of bits. Usually accessed via the >>> operator.

                      Examples:

                      • 4 >>> 2 = 1
                      • 8 >>> 2 = 2
                      • 8 >>> 3 = 1
                      • 0 >>> 3 = 0
                      • 0xf13a >>> 8 = 0xf1
                      Equations
                        Instances For
                          Equations
                            Equations
                              instance Nat.instXor :
                              Equations
                                theorem Nat.shiftLeft_eq (a b : Nat) :
                                a <<< b = a * 2 ^ b
                                @[simp]
                                theorem Nat.shiftRight_zero {n : Nat} :
                                n >>> 0 = n
                                theorem Nat.shiftRight_succ (m n : Nat) :
                                m >>> (n + 1) = m >>> n / 2
                                theorem Nat.shiftRight_add (m n k : Nat) :
                                m >>> (n + k) = m >>> n >>> k
                                theorem Nat.shiftRight_eq_div_pow (m n : Nat) :
                                m >>> n = m / 2 ^ n
                                theorem Nat.shiftRight_eq_zero (m n : Nat) (hn : m < 2 ^ n) :
                                m >>> n = 0
                                theorem Nat.shiftRight_le (m n : Nat) :
                                m >>> n m

                                testBit #

                                We define an operation for testing individual bits in the binary representation of a number.

                                def Nat.testBit (m n : Nat) :

                                Returns true if the (n+1)th least significant bit is 1, or false if it is 0.

                                Equations
                                  Instances For