Documentation

Mathlib.Data.Int.Bitwise

Bitwise operations on integers #

Recursors #

bitwise ops #

@[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
theorem Int.bit0_val (n : ) :
bit0 n = 2 * n
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
@[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]
theorem Int.bodd_bit0 (n : ) :
@[simp]
theorem Int.bodd_bit1 (n : ) :
theorem Int.bit0_ne_bit1 (m : ) (n : ) :
theorem Int.bit1_ne_bit0 (m : ) (n : ) :
@[simp]
theorem Int.testBit_zero (b : Bool) (n : ) :
@[simp]
theorem Int.testBit_succ (m : ) (b : Bool) (n : ) :
@[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.lxor' (Int.bit a m) (Int.bit b n) = Int.bit (xor a b) (Int.lxor' 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.shiftl_neg (m : ) (n : ) :
@[simp]
theorem Int.shiftr_neg (m : ) (n : ) :
@[simp]
theorem Int.shiftl_coe_nat (m : ) (n : ) :
Int.shiftl m n = ↑(Nat.shiftl m n)
@[simp]
theorem Int.shiftr_coe_nat (m : ) (n : ) :
Int.shiftr m n = ↑(Nat.shiftr m n)
@[simp]
theorem Int.shiftr_add (m : ) (n : ) (k : ) :
Int.shiftr m (n + k) = Int.shiftr (Int.shiftr m n) k

bitwise ops #

theorem Int.shiftl_add (m : ) (n : ) (k : ) :
Int.shiftl m (n + k) = Int.shiftl (Int.shiftl m n) k
theorem Int.shiftl_sub (m : ) (n : ) (k : ) :
Int.shiftl m (n - k) = Int.shiftr (Int.shiftl m n) k
theorem Int.shiftl_eq_mul_pow (m : ) (n : ) :
Int.shiftl m n = m * ↑(2 ^ n)
theorem Int.shiftr_eq_div_pow (m : ) (n : ) :
Int.shiftr m n = m / ↑(2 ^ n)
theorem Int.one_shiftl (n : ) :
Int.shiftl 1 n = ↑(2 ^ n)
@[simp]
theorem Int.zero_shiftl (n : ) :
@[simp]
theorem Int.zero_shiftr (n : ) :