Commit 2024-07-13 12:38 433fb11a

View on Github →

chore: remove autoImplicit in Util (#14694) All of them were easy to remove. Also remove on occurrence in Init/Logic which was not needed.

Estimated changes

Modified Mathlib/Init/Logic.lean

Modified Mathlib/Util/AtomM.lean

modified def Mathlib.Tactic.AtomM.run

Modified Mathlib/Util/Export.lean

modified def Lean.Export.runExportM

Modified Mathlib/Util/MemoFix.lean

Modified Mathlib/Util/Qq.lean

modified theorem Qq.QuotedDefEq.rfl

Modified Mathlib/Util/Superscript.lean

Modified Mathlib/Util/Tactic.lean

Modified Mathlib/Util/WithWeakNamespace.lean

modified def Lean.Elab.Command.withWeakNamespace