Commit 2024-07-03 14:53 bf22adb5

View on Github →

chore(Mathlib/Init): remove autoImplicit (#14355) I know Mathlib/Init is mostly going to be removed

Estimated changes

Modified Mathlib/Init/Algebra/Classes.lean

Modified Mathlib/Init/Control/Lawful.lean

Modified Mathlib/Init/Core.lean

Modified Mathlib/Init/Data/Bool/Lemmas.lean

Modified Mathlib/Init/Data/List/Basic.lean

Modified Mathlib/Init/Data/Ordering/Basic.lean

modified def Ordering.toRel

Modified Mathlib/Init/Data/Prod.lean

Modified Mathlib/Init/Data/Quot.lean

Modified Mathlib/Init/Data/Sigma/Basic.lean

modified theorem ex_of_psig

Modified Mathlib/Init/Logic.lean

modified theorem cast_proof_irrel

Modified Mathlib/Init/Quot.lean

Modified Mathlib/Init/Set.lean

modified def Set.image

Modified Mathlib/Init/ZeroOne.lean