Commit 2024-04-05 07:33 bdd38972

View on Github →

chore: Delete Init.Data.Nat.Bitwise and Init.Data.Int.Bitwise (#11898) The lemmas can easily be moved to Data.Nat.Bits and Data.Int.Bitwise respectively.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/BitVec/Defs.lean

Modified Mathlib/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.natBitwise

added def Int.testBit

Modified Mathlib/Data/Nat/Bits.lean

added def Nat.binaryRec

added theorem Nat.binaryRec_decreasing

added theorem Nat.binaryRec_eq

added theorem Nat.binaryRec_zero

added theorem Nat.bit0_val

added theorem Nat.bit1_val

added def Nat.bit

added def Nat.bitCasesOn

added theorem Nat.bit_decomp

added theorem Nat.bit_val

added theorem Nat.bit_zero

added def Nat.bits

added def Nat.bodd

added def Nat.boddDiv2

modified theorem Nat.boddDiv2_eq

added theorem Nat.bodd_add

added theorem Nat.bodd_add_div2

added theorem Nat.bodd_bit

added theorem Nat.bodd_eq_and_one_ne_zero

added theorem Nat.bodd_mul

added theorem Nat.bodd_one

added theorem Nat.bodd_succ

added theorem Nat.bodd_two

added theorem Nat.bodd_zero

added def Nat.div2

added theorem Nat.div2_bit

added theorem Nat.div2_one

added theorem Nat.div2_succ

added theorem Nat.div2_two

added theorem Nat.div2_val

added theorem Nat.div2_zero

added def Nat.ldiff

added theorem Nat.mod_two_of_bodd

added def Nat.shiftLeft'

added theorem Nat.shiftLeft'_add

added theorem Nat.shiftLeft'_false

added theorem Nat.shiftLeft'_sub

added theorem Nat.shiftLeft_add

added theorem Nat.shiftLeft_eq'

added theorem Nat.shiftLeft_sub

added theorem Nat.shiftRight_eq

added def Nat.size

added theorem Nat.testBit_bit_succ

added theorem Nat.testBit_bit_zero

Modified Mathlib/Data/Nat/Fib/Basic.lean

Modified Mathlib/Data/Num/Basic.lean

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

deleted def Int.bit

deleted def Int.bitwise

deleted def Int.bodd

deleted def Int.div2

deleted def Int.land

deleted def Int.ldiff

deleted def Int.lnot

deleted def Int.lor

deleted def Int.natBitwise

deleted def Int.testBit

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

deleted def Nat.binaryRec

deleted theorem Nat.binaryRec_decreasing

deleted theorem Nat.binaryRec_eq

deleted theorem Nat.binaryRec_zero

deleted theorem Nat.bit0_val

deleted theorem Nat.bit1_val

deleted def Nat.bit

deleted def Nat.bitCasesOn

deleted theorem Nat.bit_decomp

deleted theorem Nat.bit_val

deleted theorem Nat.bit_zero

deleted def Nat.bits

deleted def Nat.bodd

deleted def Nat.boddDiv2

deleted theorem Nat.bodd_add

deleted theorem Nat.bodd_add_div2

deleted theorem Nat.bodd_bit

deleted theorem Nat.bodd_eq_and_one_ne_zero

deleted theorem Nat.bodd_mul

deleted theorem Nat.bodd_one

deleted theorem Nat.bodd_succ

deleted theorem Nat.bodd_two

deleted theorem Nat.bodd_zero

deleted def Nat.div2

deleted theorem Nat.div2_bit

deleted theorem Nat.div2_one

deleted theorem Nat.div2_succ

deleted theorem Nat.div2_two

deleted theorem Nat.div2_val

deleted theorem Nat.div2_zero

deleted def Nat.ldiff

deleted theorem Nat.mod_two_of_bodd

deleted def Nat.shiftLeft'

deleted theorem Nat.shiftLeft'_add

deleted theorem Nat.shiftLeft'_false

deleted theorem Nat.shiftLeft'_sub

deleted theorem Nat.shiftLeft_add

deleted theorem Nat.shiftLeft_eq'

deleted theorem Nat.shiftLeft_sub

deleted theorem Nat.shiftRight_eq

deleted def Nat.size

deleted theorem Nat.testBit_bit_succ

deleted theorem Nat.testBit_bit_zero