Commit 2024-07-09 11:47 a01fca80

View on Github →

chore(Data): reduce use of autoImplicit (#14362) This is not exhaustive: there are about ten remaining files in this directory. Data/Vector may come in a follow-up PR (this is harder).

Estimated changes

Modified Mathlib/Data/Array/ExtractLemmas.lean

modified theorem Array.extract_eq_of_size_le_end

modified theorem Array.extract_extract

Modified Mathlib/Data/ByteArray.lean

modified def ByteSlice.forIn.loop

Modified Mathlib/Data/List/Range.lean

modified theorem List.indexOf_finRange

modified theorem List.range'_one

Modified Mathlib/Data/Matroid/Basic.lean

modified theorem Matroid.Base.exchange

modified theorem Matroid.Base.exchange_mem

modified theorem Matroid.Base.finite_of_finite

modified theorem Matroid.Base.insert_not_base

modified theorem Matroid.Base.not_base_of_ssubset

modified theorem Matroid.ExchangeProperty.encard_diff_le_aux

modified theorem Matroid.Indep.base_of_forall_insert

Modified Mathlib/Data/Stream/Defs.lean

Modified Mathlib/Data/Stream/Init.lean

modified theorem Stream'.concat_take_get

modified theorem Stream'.dropLast_take

modified theorem Stream'.drop_tail'

modified theorem Stream'.get_tail

modified theorem Stream'.tail_drop'

modified theorem Stream'.take_succ_cons

Modified Mathlib/Data/Sym/Basic.lean

Modified Mathlib/Data/UnionFind.lean