Commit 2023-10-19 09:56 b9ac893f

View on Github →

refactor: use bitwise notation for Nat.land, Nat.lor, and Nat.xor (#7759) This didn't exist in Lean 3.

Estimated changes

modified theorem Nat.land_assoc
modified theorem Nat.land_bit
modified theorem Nat.land_comm
modified theorem Nat.land_zero
modified theorem Nat.lor_assoc
modified theorem Nat.lor_bit
modified theorem Nat.lor_comm
modified theorem Nat.lor_zero
modified theorem Nat.lt_xor_cases
modified theorem Nat.lxor_cancel_right
modified theorem Nat.testBit_land
modified theorem Nat.testBit_lor
modified theorem Nat.testBit_xor
modified theorem Nat.xor_assoc
modified theorem Nat.xor_bit
modified theorem Nat.xor_cancel_left
modified theorem Nat.xor_comm
modified theorem Nat.xor_eq_zero
modified theorem Nat.xor_left_inj
modified theorem Nat.xor_left_injective
modified theorem Nat.xor_ne_zero
modified theorem Nat.xor_right_inj
modified theorem Nat.xor_right_injective
modified theorem Nat.xor_self
modified theorem Nat.xor_trichotomy
modified theorem Nat.xor_zero
modified theorem Nat.zero_land
modified theorem Nat.zero_lor
modified theorem Nat.zero_xor