Commit 2024-04-07 02:48 a7ffab83

View on Github →

chore(Data/Int/Cast): fix confusion between OfNat and Nat.cast lemmas (#11861) This renames

  • Int.cast_ofNat to Int.cast_natCast
  • Int.int_cast_ofNat to Int.cast_ofNat I think the history here is that this lemma was previously about Int.ofNat, before we globally fixed the simp-normal form to be Nat.cast. Since the Int.cast_ofNat name is repurposed, it can't be deprecated. Int.int_cast_ofNat is such a wonky name that it was probably never used.

Estimated changes

modified theorem Int.ceil_add_nat
modified theorem Int.floor_add_nat
modified theorem Int.floor_sub_nat
modified theorem Int.cast_four
added theorem Int.cast_natCast
modified theorem Int.cast_ofNat
modified theorem Int.cast_three
modified theorem Int.cast_two
deleted theorem Int.int_cast_ofNat