Commit 2022-11-23 03:12 76b3234c

View on Github →

feat: port Data.Int.Cast.Basic (#670) mathlib3 SHA: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3 Porting notes:

  1. Some lemmas were transferred from Data.Int.Cast.Defs in order to match mathlib3 (I accidentally put them in the wrong place when I had ported that file because those lemmas were already present in mathlib4.)
  2. The lemmas just mentioned have retained their simp attribute for the reason Gabriel mentioned on that PR (#641), even though that attribute isn't present on the mathlib3 version.
  3. The bit0 and bit1 lemmas have been marked as deprecated.
  4. There were many dubious translation errors, I believe primarily because of the difference in the way coercions are handled, so I have #aligned all of these with ₓ. I believe this is the correct thing to do, but confirmation would be nice.

Estimated changes

modified theorem Int.cast_add
added theorem Int.cast_bit0
added theorem Int.cast_bit1
added theorem Int.cast_four
modified theorem Int.cast_neg
added theorem Int.cast_negOfNat
added theorem Int.cast_negSucc
added theorem Int.cast_ofNat
added theorem Int.cast_one
modified theorem Int.cast_sub
modified theorem Int.cast_subNatNat
added theorem Int.cast_three
added theorem Int.cast_two
added theorem Int.cast_zero
added theorem Int.ofNat_bit0
added theorem Int.ofNat_bit1
added theorem Nat.cast_pred
deleted theorem Int.cast_negSucc
deleted theorem Int.cast_ofNat
deleted theorem Int.cast_one
deleted theorem Int.cast_zero