Commit 2024-06-07 03:20 bbf0d1e3

View on Github →

chore: merge bump/v4.9.0 (#13584) This has all been reviewed in PRs from bump/nightly-2024-MM-DD branches to the bump/v4.9.0, and now needs to come to master!

Estimated changes

modified theorem Nat.Up.WF
modified theorem Nat.Up.next
modified def Nat.Up
modified def Nat.upRel
deleted theorem Char.ofNat_toNat
deleted def Char.toUInt8
deleted theorem Char.utf8Size_pos
added theorem Int.shiftRight_add'
deleted theorem Int.shiftRight_add
deleted theorem Int.shiftRight_eq_div_pow
added theorem Int.zero_shiftRight'
deleted theorem Int.zero_shiftRight
modified theorem Commute.intCast_mul_self
deleted theorem Nat.shiftLeft_add
modified theorem Nat.multinomial_empty
modified def Nat.minFacAux
modified theorem Rat.mk'_zero
deleted theorem $typeName.add_def
deleted theorem $typeName.eq_of_val_eq
deleted theorem $typeName.mk_val_eq
deleted theorem $typeName.mod_def
deleted theorem $typeName.mul_def
deleted theorem $typeName.one_def
deleted theorem $typeName.sub_def
deleted theorem $typeName.val_eq_of_eq
deleted theorem $typeName.zero_def
deleted theorem UInt16.val_eq_of_lt
deleted theorem UInt32.val_eq_of_lt
deleted theorem UInt64.val_eq_of_lt
deleted theorem UInt8.val_eq_of_lt
deleted theorem USize.val_eq_of_lt