Bitwise

📁 Source: Mathlib/Data/Int/Bitwise.lean

Statistics

Metric	Count
Definitions bit, bitCasesOn, bitwise, bodd, div2, instShiftLeft_mathlib, instShiftRight_mathlib, land, ldiff, lnot, lor, natBitwise, xor	13
Theorems bit_coe_nat, bit_decomp, bit_negSucc, bit_val, bit_zero, bitwise_and, bitwise_bit, bitwise_diff, bitwise_or, bitwise_xor, bodd_add, bodd_add_div2, bodd_bit, bodd_coe, bodd_mul, bodd_neg, bodd_negOfNat, bodd_one, bodd_subNatNat, bodd_two, bodd_zero, div2_val, land_bit, ldiff_bit, lnot_bit, lor_bit, lxor_bit, one_shiftLeft, shiftLeft_add', shiftLeft_eq_mul_pow, shiftLeft_natCast, shiftLeft_natCast_right, shiftLeft_neg, shiftLeft_negSucc, shiftLeft_sub, shiftRight_add', shiftRight_natCast, shiftRight_natCast_right, shiftRight_neg, shiftRight_negSucc, testBit_bit_succ, testBit_bit_zero, testBit_bitwise, testBit_land, testBit_ldiff, testBit_lnot, testBit_lor, testBit_lxor, zero_shiftLeft', zero_shiftRight'	50
Total	63

Int

Definitions

Name	Category	Theorems
bit 📖	CompOp	15 math math: bodd_bit, testBit_bit_succ, testBit_bit_zero, bit_negSucc, bit_coe_nat, lxor_bit, lnot_bit, ldiff_bit, bit_zero, land_bit, bitwise_bit, bit_val, lor_bit, div2_bit, bit_decomp
bitCasesOn 📖	CompOp	—
bitwise 📖	CompOp	6 math math: bitwise_diff, testBit_bitwise, bitwise_or, bitwise_bit, bitwise_and, bitwise_xor
bodd 📖	CompOp	9 math, 3 bridge math: bodd_bit, bodd_add, bodd_negOfNat, bodd_add_div2, bodd_subNatNat, bodd_neg, bodd_mul, bodd_coe, bit_decomp bridge: bodd_zero, bodd_one, bodd_two
div2 📖	CompOp	4 math math: bodd_add_div2, div2_val, div2_bit, bit_decomp
instShiftLeft_mathlib 📖	CompOp	10 math math: shiftLeft_natCast, shiftLeft_negSucc, shiftLeft_add', shiftLeft_natCast_right, shiftLeft_eq_mul_pow, zero_shiftLeft', shiftRight_neg, one_shiftLeft, shiftLeft_neg, shiftLeft_sub
instShiftRight_mathlib 📖	CompOp	8 math math: shiftRight_natCast_right, shiftRight_negSucc, zero_shiftRight', shiftRight_natCast, shiftRight_add', shiftRight_neg, shiftLeft_neg, shiftLeft_sub
land 📖	CompOp	3 math math: testBit_land, land_bit, bitwise_and
ldiff 📖	CompOp	3 math math: testBit_ldiff, bitwise_diff, ldiff_bit
lnot 📖	CompOp	2 math math: lnot_bit, testBit_lnot
lor 📖	CompOp	3 math math: testBit_lor, bitwise_or, lor_bit
natBitwise 📖	CompOp	—
xor 📖	CompOp	3 math math: testBit_lxor, lxor_bit, bitwise_xor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bit_coe_nat 📖	mathematical	—	bit Nat.bit	—	bit_val Nat.bit_val
bit_decomp 📖	mathematical	—	bit bodd div2	—	bit_val add_comm bodd_add_div2
bit_negSucc 📖	mathematical	—	bit Nat.bit	—	bit_val Nat.bit_val
bit_val 📖	mathematical	—	bit	—	add_zero
bit_zero 📖	mathematical	—	bit	—	—
bitwise_and 📖	mathematical	—	bitwise land	—	Nat.bitwise_swap Function.swap.eq_1
bitwise_bit 📖	mathematical	—	bitwise bit	—	bit_coe_nat Nat.bitwise_bit bit_negSucc
bitwise_diff 📖	mathematical	—	bitwise ldiff	—	Nat.bitwise_swap Function.swap.eq_1
bitwise_or 📖	mathematical	—	bitwise lor	—	Nat.bitwise_swap Function.swap.eq_1
bitwise_xor 📖	mathematical	—	bitwise xor	—	Bool.bne_eq_xor
bodd_add 📖	mathematical	—	bodd	—	Nat.bodd_add bodd_subNatNat Nat.bodd_succ
bodd_add_div2 📖	mathematical	—	bodd div2	—	Nat.bodd_add_div2 zero_add add_comm
bodd_bit 📖	mathematical	—	bodd bit	—	bit_val add_zero bodd_mul bodd_add
bodd_coe 📖	mathematical	—	bodd Nat.bodd	—	—
bodd_mul 📖	mathematical	—	bodd	—	Nat.bodd_mul bodd_neg
bodd_neg 📖	mathematical	—	bodd	—	bodd_negOfNat Nat.bodd_succ
bodd_negOfNat 📖	mathematical	—	bodd Nat.bodd	—	Nat.bodd_succ
bodd_one 📖	bridging (complete)	—	bodd	bodd	—
bodd_subNatNat 📖	mathematical	—	bodd Nat.bodd	—	Nat.bodd_add Nat.bodd_succ
bodd_two 📖	bridging (complete)	—	bodd	bodd	—
bodd_zero 📖	bridging (complete)	—	bodd	bodd	—
div2_val 📖	mathematical	—	div2	—	Nat.div2_val
land_bit 📖	mathematical	—	land bit	—	bitwise_and bitwise_bit
ldiff_bit 📖	mathematical	—	ldiff bit	—	bitwise_diff bitwise_bit
lnot_bit 📖	mathematical	—	lnot bit	—	bit_coe_nat bit_negSucc
lor_bit 📖	mathematical	—	lor bit	—	bitwise_or bitwise_bit
lxor_bit 📖	mathematical	—	xor bit	—	bitwise_xor bitwise_bit
one_shiftLeft 📖	mathematical	—	instShiftLeft_mathlib Monoid.toNatPow Nat.instMonoid	—	Nat.shiftLeft'_false one_mul
shiftLeft_add' 📖	mathematical	—	instShiftLeft_mathlib	—	Nat.shiftLeft'_false mul_assoc Nat.shiftLeft'_add shiftLeft_natCast Nat.shiftLeft_sub le_rfl Nat.cast_one Nat.shiftLeft'_sub add_assoc Nat.shiftLeft'.eq_1
shiftLeft_eq_mul_pow 📖	mathematical	—	instShiftLeft_mathlib Monoid.toNatPow Nat.instMonoid	—	Nat.shiftLeft'_false Nat.shiftLeft'_tt_eq_mul_pow
shiftLeft_natCast 📖	mathematical	—	instShiftLeft_mathlib	—	Nat.shiftLeft'_false
shiftLeft_natCast_right 📖	mathematical	—	instShiftLeft_mathlib	—	Nat.instAtLeastTwoHAddOfNat Nat.shiftLeft'_false Nat.shiftLeft'_tt_eq_mul_pow
shiftLeft_neg 📖	mathematical	—	instShiftLeft_mathlib instShiftRight_mathlib	—	—
shiftLeft_negSucc 📖	mathematical	—	instShiftLeft_mathlib Nat.shiftLeft'	—	—
shiftLeft_sub 📖	mathematical	—	instShiftLeft_mathlib instShiftRight_mathlib	—	shiftLeft_add'
shiftRight_add' 📖	mathematical	—	instShiftRight_mathlib	—	shiftRight_natCast shiftRight_negSucc
shiftRight_natCast 📖	mathematical	—	instShiftRight_mathlib	—	—
shiftRight_natCast_right 📖	mathematical	—	instShiftRight_mathlib	—	shiftRight_natCast shiftRight_negSucc
shiftRight_neg 📖	mathematical	—	instShiftRight_mathlib instShiftLeft_mathlib	—	shiftLeft_neg neg_neg
shiftRight_negSucc 📖	mathematical	—	instShiftRight_mathlib	—	—
testBit_bit_succ 📖	mathematical	—	bit	—	bit_coe_nat Nat.testBit_bit_succ bit_negSucc
testBit_bit_zero 📖	mathematical	—	bit	—	bit_coe_nat Nat.testBit_bit_zero bit_negSucc
testBit_bitwise 📖	mathematical	—	bitwise	—	—
testBit_land 📖	mathematical	—	land	—	bitwise_and testBit_bitwise
testBit_ldiff 📖	mathematical	—	ldiff	—	bitwise_diff testBit_bitwise
testBit_lnot 📖	mathematical	—	lnot	—	—
testBit_lor 📖	mathematical	—	lor	—	bitwise_or testBit_bitwise
testBit_lxor 📖	mathematical	—	xor	—	bitwise_xor testBit_bitwise
zero_shiftLeft' 📖	mathematical	—	instShiftLeft_mathlib	—	Nat.shiftLeft'_false
zero_shiftRight' 📖	mathematical	—	instShiftRight_mathlib	—	zero_shiftLeft'

---

← Back to Index