Documentation

Mathlib.Data.Int.Bitwise

Bitwise operations on integers #

Recursors #

bitwise ops #

@[simp]
@[simp]
@[simp]
theorem Int.bodd_coe (n : ) :
@[simp]
@[simp]
theorem Int.bodd_neg (n : ) :
@[simp]
theorem Int.bodd_add (m : ) (n : ) :
@[simp]
theorem Int.bodd_mul (m : ) (n : ) :
theorem Int.bodd_add_div2 (n : ) :
(bif Int.bodd n then 1 else 0) + 2 * Int.div2 n = n
theorem Int.div2_val (n : ) :
Int.div2 n = n / 2
@[deprecated]
theorem Int.bit0_val (n : ) :
bit0 n = 2 * n
@[deprecated]
theorem Int.bit1_val (n : ) :
bit1 n = 2 * n + 1
theorem Int.bit_val (b : Bool) (n : ) :
Int.bit b n = 2 * n + bif b then 1 else 0
def Int.bitCasesOn {C : Sort u} (n : ) (h : (b : Bool) → (n : ) → C (Int.bit b n)) :
C n

Defines a function from conditionally, if it is defined for odd and even integers separately using bit.

Equations
Instances For
    @[simp]
    @[simp]
    theorem Int.bit_coe_nat (b : Bool) (n : ) :
    Int.bit b n = (Nat.bit b n)
    @[simp]
    theorem Int.bit_negSucc (b : Bool) (n : ) :
    @[simp]
    theorem Int.bodd_bit (b : Bool) (n : ) :
    @[simp, deprecated]
    theorem Int.bodd_bit0 (n : ) :
    @[simp, deprecated]
    theorem Int.bodd_bit1 (n : ) :
    @[deprecated]
    theorem Int.bit0_ne_bit1 (m : ) (n : ) :
    @[deprecated]
    theorem Int.bit1_ne_bit0 (m : ) (n : ) :
    @[deprecated]
    theorem Int.bit1_ne_zero (m : ) :
    bit1 m 0
    @[simp]
    theorem Int.testBit_bit_zero (b : Bool) (n : ) :
    @[simp]
    theorem Int.testBit_bit_succ (m : ) (b : Bool) (n : ) :
    theorem Int.bitwise_diff :
    (Int.bitwise fun (a b : Bool) => a && !b) = Int.ldiff
    @[simp]
    theorem Int.bitwise_bit (f : BoolBoolBool) (a : Bool) (m : ) (b : Bool) (n : ) :
    Int.bitwise f (Int.bit a m) (Int.bit b n) = Int.bit (f a b) (Int.bitwise f m n)
    @[simp]
    theorem Int.lor_bit (a : Bool) (m : ) (b : Bool) (n : ) :
    Int.lor (Int.bit a m) (Int.bit b n) = Int.bit (a || b) (Int.lor m n)
    @[simp]
    theorem Int.land_bit (a : Bool) (m : ) (b : Bool) (n : ) :
    Int.land (Int.bit a m) (Int.bit b n) = Int.bit (a && b) (Int.land m n)
    @[simp]
    theorem Int.ldiff_bit (a : Bool) (m : ) (b : Bool) (n : ) :
    Int.ldiff (Int.bit a m) (Int.bit b n) = Int.bit (a && !b) (Int.ldiff m n)
    @[simp]
    theorem Int.lxor_bit (a : Bool) (m : ) (b : Bool) (n : ) :
    Int.xor (Int.bit a m) (Int.bit b n) = Int.bit (xor a b) (Int.xor m n)
    @[simp]
    theorem Int.lnot_bit (b : Bool) (n : ) :
    @[simp]
    theorem Int.testBit_bitwise (f : BoolBoolBool) (m : ) (n : ) (k : ) :
    @[simp]
    theorem Int.testBit_lor (m : ) (n : ) (k : ) :
    @[simp]
    theorem Int.testBit_land (m : ) (n : ) (k : ) :
    @[simp]
    theorem Int.testBit_ldiff (m : ) (n : ) (k : ) :
    @[simp]
    theorem Int.testBit_lxor (m : ) (n : ) (k : ) :
    @[simp]
    theorem Int.testBit_lnot (n : ) (k : ) :
    @[simp]
    theorem Int.shiftLeft_neg (m : ) (n : ) :
    m <<< (-n) = m >>> n
    @[simp]
    theorem Int.shiftRight_neg (m : ) (n : ) :
    m >>> (-n) = m <<< n
    @[simp]
    theorem Int.shiftLeft_coe_nat (m : ) (n : ) :
    m <<< n = (m <<< n)
    @[simp]
    theorem Int.shiftRight_coe_nat (m : ) (n : ) :
    m >>> n = (m >>> n)
    @[simp]
    theorem Int.shiftRight_negSucc (m : ) (n : ) :
    theorem Int.shiftRight_add (m : ) (n : ) (k : ) :
    m >>> (n + k) = m >>> n >>> k

    bitwise ops #

    theorem Int.shiftLeft_add (m : ) (n : ) (k : ) :
    m <<< (n + k) = m <<< n <<< k
    theorem Int.shiftLeft_sub (m : ) (n : ) (k : ) :
    m <<< (n - k) = m <<< n >>> k
    theorem Int.shiftLeft_eq_mul_pow (m : ) (n : ) :
    m <<< n = m * (2 ^ n)
    theorem Int.shiftRight_eq_div_pow (m : ) (n : ) :
    m >>> n = m / (2 ^ n)
    theorem Int.one_shiftLeft (n : ) :
    1 <<< n = (2 ^ n)
    @[simp]
    theorem Int.zero_shiftLeft (n : ) :
    0 <<< n = 0
    @[simp]
    theorem Int.zero_shiftRight (n : ) :
    0 >>> n = 0