Commit 2022-07-11 12:59 8f609e0e

View on Github →

chore: bump to nightly-2022-07-11 (#300)

Estimated changes

Modified Mathlib/Data/Array/Basic.lean

added theorem Array.data_get?_eq_getElem?

added theorem Array.data_get_eq_getElem

deleted theorem Array.data_toArray

deleted theorem Array.ext'

deleted theorem Array.get?_eq_get

deleted theorem Array.get?_eq_get?

added theorem Array.get?_eq_getElem?

modified theorem Array.get?_len_le

modified theorem Array.get?_push_eq

modified theorem Array.get?_set

modified theorem Array.get?_set_eq

modified theorem Array.get?_set_ne

added theorem Array.getData_eq_getElem

added theorem Array.getElem?_eq_get

deleted theorem Array.get_eq_get

added theorem Array.get_eq_getElem

modified theorem Array.get_push

added theorem Array.get_push_eq

added theorem Array.get_push_lt

added theorem Array.get_set

added theorem Array.get_set_eq

added theorem Array.get_set_ne

deleted theorem Array.toArrayLit_eq'

added theorem Array.toArray_data

added theorem getElem?_neg

added theorem getElem?_pos

Modified Mathlib/Data/Fin/Basic.lean

deleted theorem Fin.mod_eq

deleted theorem Fin.mod_eq_val

deleted theorem Fin.modn_def

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.concat_eq_append

deleted theorem List.drop_eq_nil_of_le

modified theorem List.get?_concat_length

Modified Mathlib/Data/UnionFind.lean

Modified Mathlib/Init/Logic.lean

Modified Mathlib/Tactic/Have.lean

Modified Mathlib/Tactic/Lint/Frontend.lean

Modified Mathlib/Tactic/NoMatch.lean

Modified Mathlib/Tactic/NormNum.lean

added theorem Lean.Meta.NormNum.isNat_cast

Modified Mathlib/Tactic/RCases.lean

Modified Mathlib/Tactic/Ring.lean

Modified Mathlib/Tactic/ToAdditive.lean

Modified Mathlib/Testing/SlimCheck/Testable.lean

Modified lean-toolchain