Commit 2024-07-19 05:13 b5f3b59f

View on Github →

chore(Mathlib/Lean): remove use of autoImplicit (#14884) All eleven files in the Lean/ directory use autoImplicit, but only in a very minor way. Removing it seems easier than making this a permanent exception.

Estimated changes

Modified Mathlib/Lean/CoreM.lean

modified def CoreM.withImportModules

Modified Mathlib/Lean/Elab/Tactic/Basic.lean

modified def Lean.Elab.Tactic.focusAndDoneWithScope

Modified Mathlib/Lean/EnvExtension.lean

Modified Mathlib/Lean/Exception.lean

modified def successIfFail

Modified Mathlib/Lean/Expr/Basic.lean

modified def Lean.Expr.modifyAppArgM

modified def Lean.Expr.modifyArgM

Modified Mathlib/Lean/Message.lean

Modified Mathlib/Lean/Meta.lean

Modified Mathlib/Lean/Meta/Basic.lean

modified def Lean.Meta.preservingMCtx

Modified Mathlib/Lean/Meta/DiscrTree.lean

Modified Mathlib/Lean/Meta/Simp.lean

added def Lean.PHashSet.toList.{u}

deleted def Lean.PHashSet.toList

Modified Mathlib/Lean/Thunk.lean

modified theorem Thunk.prod_get_fst

modified theorem Thunk.prod_get_snd