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