Commit 2023-01-02 08:14 bd486945

View on Github →

feat: port Data.Int.Bitwise (#1159) This seems to be ready for review and merge now. There's only one question about renaming shiftl_coe_nat and shiftr_coe_nat left.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Int/Bitwise.lean

added theorem Int.bit0_ne_bit1

added theorem Int.bit0_val

added theorem Int.bit1_ne_bit0

added theorem Int.bit1_ne_zero

added theorem Int.bit1_val

added def Int.bitCasesOn.{u}

added theorem Int.bit_coe_nat

added theorem Int.bit_decomp

added theorem Int.bit_negSucc

added theorem Int.bit_val

added theorem Int.bit_zero

added theorem Int.bitwise_and

added theorem Int.bitwise_bit

added theorem Int.bitwise_diff

added theorem Int.bitwise_or

added theorem Int.bitwise_xor

added theorem Int.bodd_add

added theorem Int.bodd_add_div2

added theorem Int.bodd_bit0

added theorem Int.bodd_bit1

added theorem Int.bodd_bit

added theorem Int.bodd_coe

added theorem Int.bodd_mul

added theorem Int.bodd_neg

added theorem Int.bodd_negOfNat

added theorem Int.bodd_one

added theorem Int.bodd_subNatNat

added theorem Int.bodd_two

added theorem Int.bodd_zero

added theorem Int.div2_val

added theorem Int.land_bit

added theorem Int.ldiff_bit

added theorem Int.lnot_bit

added theorem Int.lor_bit

added theorem Int.lxor_bit

added theorem Int.one_shiftl

added theorem Int.shiftl_add

added theorem Int.shiftl_coe_nat

added theorem Int.shiftl_eq_mul_pow

added theorem Int.shiftl_neg

added theorem Int.shiftl_negSucc

added theorem Int.shiftl_sub

added theorem Int.shiftr_add

added theorem Int.shiftr_coe_nat

added theorem Int.shiftr_eq_div_pow

added theorem Int.shiftr_neg

added theorem Int.shiftr_negSucc

added theorem Int.testBit_bitwise

added theorem Int.testBit_land

added theorem Int.testBit_ldiff

added theorem Int.testBit_lnot

added theorem Int.testBit_lor

added theorem Int.testBit_lxor

added theorem Int.testBit_succ

added theorem Int.testBit_zero

added theorem Int.zero_shiftl

added theorem Int.zero_shiftr

Created Mathlib/Init/Data/Int/Bitwise.lean

added def Int.bit

added def Int.bitwise

added def Int.bodd

added def Int.div2

added def Int.land

added def Int.ldiff'

added def Int.lnot

added def Int.lor

added def Int.lxor'

added def Int.natBitwise

added def Int.shiftl

added def Int.shiftr

added def Int.testBit

Modified Mathlib/Init/Data/Nat/Bitwise.lean