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 : Nat) (m : Nat) :
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[extern lean_nat_land]
    def Nat.land :
    NatNatNat
    Equations
    Instances For
      @[extern lean_nat_lor]
      def Nat.lor :
      NatNatNat
      Equations
      Instances For
        @[extern lean_nat_lxor]
        def Nat.xor :
        NatNatNat
        Equations
        Instances For
          @[extern lean_nat_shiftl]
          def Nat.shiftLeft :
          NatNatNat
          Equations
          • x.shiftLeft 0 = x
          • x.shiftLeft m.succ = (2 * x).shiftLeft m
          Instances For
            @[extern lean_nat_shiftr]
            def Nat.shiftRight :
            NatNatNat
            Equations
            • x.shiftRight 0 = x
            • x.shiftRight m.succ = x.shiftRight m / 2
            Instances For
              Equations
              Equations
              instance Nat.instXor :
              Equations
              theorem Nat.shiftLeft_eq (a : Nat) (b : Nat) :
              a <<< b = a * 2 ^ b
              @[simp]
              theorem Nat.shiftRight_zero {n : Nat} :
              n >>> 0 = n
              theorem Nat.shiftRight_succ (m : Nat) (n : Nat) :
              m >>> (n + 1) = m >>> n / 2
              theorem Nat.shiftRight_add (m : Nat) (n : Nat) (k : Nat) :
              m >>> (n + k) = m >>> n >>> k
              theorem Nat.shiftRight_eq_div_pow (m : Nat) (n : Nat) :
              m >>> n = m / 2 ^ n

              testBit #

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

              def Nat.testBit (m : Nat) (n : Nat) :

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

              Equations
              Instances For