Commit 2023-08-25 13:22 89686db4

View on Github →

feat: delete Nat.shiftr and Nat.shiftl (#6356) These already exists upstream (with minorly different but equal definitions) as Nat.shiftRight and Nat.shiftLeft.

Estimated changes

modified theorem Int.shiftl_coe_nat
modified theorem Int.shiftr_coe_nat
modified theorem Int.shiftr_negSucc
modified theorem Nat.zero_testBit
deleted theorem Nat.one_shiftl
deleted theorem Nat.shiftl_eq_mul_pow
deleted theorem Nat.shiftr_eq_div_pow
added theorem Nat.size_shiftLeft
deleted theorem Nat.size_shiftl
added theorem Nat.zero_shiftLeft
deleted theorem Nat.zero_shiftl
deleted theorem Nat.zero_shiftr
modified theorem Num.shiftl_to_nat
modified theorem Num.shiftr_to_nat
added theorem Nat.shiftLeft_add
added theorem Nat.shiftLeft_eq'
added theorem Nat.shiftLeft_sub
added theorem Nat.shiftLeft_succ
added theorem Nat.shiftLeft_zero
added theorem Nat.shiftRight_add
added theorem Nat.shiftRight_eq
added theorem Nat.shiftRight_succ
added theorem Nat.shiftRight_zero
added theorem Nat.shiftl'_false
modified theorem Nat.shiftl'_sub
deleted def Nat.shiftl
deleted theorem Nat.shiftl_add
deleted theorem Nat.shiftl_sub
deleted theorem Nat.shiftl_succ
deleted theorem Nat.shiftl_zero
deleted def Nat.shiftr
deleted theorem Nat.shiftr_add
deleted theorem Nat.shiftr_zero
added theorem Nat.zero_shiftRight