Commit 2024-07-15 23:26 4b7d7ade
View on Github →chore: remove lemmas about bit0/bit1 (#14765) remove many occurences of set_option linter.deprecated false Deletions:
- bit0_add
- bit0_left
- bit0_mul
- bit0_neg
- bit0_right
- bit1_add
- bit1_add'
- bit1_left
- bit1_mul
- bit1_right
- bit_le_bit1_iff
- bit_le_bit_iff
- bit_lt_bit_iff
- I_pow_bit0
- I_pow_bit1
- mul_bit0
- mul_bit1
- neg_pow_bit0
- neg_pow_bit1
- one_le_bit0_iff
- one_lt_bit0_iff
- pow_bit0
- pow_bit0'
- pow_bit1
- pow_bit1'
- size_bit0
- size_bit1