Commit 2023-10-12 12:34 11458852

View on Github →

feat(Data/Num): use bitwise notation (#7593) This enables the existing |||, &&&, <<<, >>>, and ^^^ notation for Num and PosNum, and makes them simp-normal form.

Estimated changes

Modified Mathlib/Data/Num/Bitwise.lean

added theorem Num.land_eq_and

deleted def Num.lor

added theorem Num.lor_eq_or

added theorem Num.lxor_eq_xor

added theorem Num.shiftl_eq_shiftLeft

added theorem Num.shiftr_eq_shiftRight

added theorem PosNum.land_eq_and

added theorem PosNum.lor_eq_or

added theorem PosNum.lxor_eq_xor

added theorem PosNum.shiftl_eq_shiftLeft

modified theorem PosNum.shiftl_succ_eq_bit0_shiftl

added theorem PosNum.shiftr_eq_shiftRight

Modified Mathlib/Data/Num/Lemmas.lean

modified theorem Num.land'_to_nat

modified theorem Num.ldiff'_to_nat

modified theorem Num.lor'_to_nat

modified theorem Num.lxor'_to_nat

modified theorem Num.shiftl_to_nat

modified theorem Num.shiftr_to_nat