Commit 2024-10-20 12:27 6a88b546

View on Github →

chore: move binary recursion on Nat into a new file (#15567) This is #13649 with fewer definition changes.

Estimated changes

added def Nat.binaryRec'
added def Nat.binaryRec
added theorem Nat.binaryRec_eq'
added theorem Nat.binaryRec_eq
added theorem Nat.binaryRec_one
added theorem Nat.binaryRec_zero
added def Nat.bit
added def Nat.bitCasesOn
added theorem Nat.bitCasesOn_bit
added theorem Nat.bit_div_two
added theorem Nat.bit_eq_zero_iff
added theorem Nat.bit_mod_two
added theorem Nat.bit_shiftRight_one
added theorem Nat.bit_val
added theorem Nat.shiftRight_one
added theorem Nat.testBit_bit_zero
deleted def Nat.binaryRec'
deleted def Nat.binaryRec
deleted theorem Nat.binaryRec_eq'
deleted theorem Nat.binaryRec_eq
deleted theorem Nat.binaryRec_one
deleted theorem Nat.binaryRec_zero
deleted def Nat.bit
deleted def Nat.bitCasesOn
deleted theorem Nat.bitCasesOn_bit
deleted theorem Nat.bit_div_two
deleted theorem Nat.bit_eq_zero_iff
deleted theorem Nat.bit_shiftRight_one
deleted theorem Nat.bit_val
deleted theorem Nat.shiftRight_one
deleted theorem Nat.testBit_bit_zero
deleted theorem Nat.bit_mod_two