Commit 2024-10-18 13:37 8f520637

View on Github →

chore: redefine Nat.bitCasesOn Nat.binaryRec (#15571) The new definitions of Nat.bitCasesOn and Nat.binaryRec* have better runtime performance. Also they have lighter weight dependencies now and may be upstreamed to Batteries later.

Estimated changes

modified def Nat.binaryRec'
modified def Nat.binaryRec
modified def Nat.binaryRecFromOne
modified theorem Nat.binaryRec_eq'
modified theorem Nat.binaryRec_eq
modified theorem Nat.binaryRec_zero
modified def Nat.bitCasesOn
modified theorem Nat.bitCasesOn_bit0
modified theorem Nat.bitCasesOn_bit1
modified theorem Nat.bitCasesOn_bit
modified theorem Nat.bit_cases_on_inj
modified theorem Nat.bit_cases_on_injective
added theorem Nat.bit_div_two
added theorem Nat.bit_shiftRight_one
added theorem Nat.shiftRight_one