Commit 2025-01-05 03:32 0f181024

View on Github →

chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464)

Estimated changes

modified theorem Fin.cast_eq_cast
modified theorem Fin.cast_eq_self
modified theorem Fin.cast_le_cast
modified theorem Fin.cast_lt_cast
modified theorem Fin.cast_zero
modified theorem Fin.leftInverse_cast
modified theorem Fin.rightInverse_cast
deleted theorem List.Lex.not_nil_right
deleted inductive List.Lex
modified theorem List.lt_iff_lex_lt
deleted theorem List.nil_le
deleted theorem List.nil_lt_cons
modified def ONote.ofNat
modified theorem ONote.ofNat_one
modified theorem ONote.repr_ofNat
modified theorem ONote.repr_one
added theorem ONote.repr_zero