Commit 2024-08-27 19:30 6e2fa8b6

View on Github →

chore: remove autoImplicit from Archive, Cache, Data (#16187) Split from #16154 – this PR contains just the less contentious changes. Four non-test files will remain after this.

Estimated changes

Modified Archive/Examples/IfNormalization/Result.lean

modified theorem IfExpr.eval_ite_ite

modified theorem IfExpr.eval_lit

modified theorem IfExpr.eval_var

Modified Archive/Examples/IfNormalization/WithoutAesop.lean

modified theorem IfExpr.eval_ite_ite'

Modified Cache/IO.lean

Modified Cache/Requests.lean

modified def Cache.Requests.formatError

Modified Mathlib/Data/MLList/BestFirst.lean

Modified Mathlib/Data/Vector/Basic.lean

modified theorem Mathlib.Vector.mapAccumr_cons

modified theorem Mathlib.Vector.mapAccumr₂_cons

Modified Mathlib/Data/Vector/Defs.lean

modified def Mathlib.Vector.mapAccumr₂

Modified Mathlib/Data/Vector/MapLemmas.lean

modified theorem Mathlib.Vector.mapAccumr_map

modified theorem Mathlib.Vector.map_mapAccumr

Modified Mathlib/Data/Vector/Snoc.lean

modified theorem Mathlib.Vector.mapAccumr_nil

modified theorem Mathlib.Vector.mapAccumr_snoc

modified theorem Mathlib.Vector.mapAccumr₂_nil

modified theorem Mathlib.Vector.map_snoc

modified theorem Mathlib.Vector.map₂_snoc

Modified Mathlib/Deprecated/HashMap.lean

Modified Mathlib/Topology/MetricSpace/Gluing.lean