Commit 2023-06-25 11:21 52d95f2b

View on Github →

chore: disable relaxedAutoImplicit (#5277) We disable the "relaxed" auto-implicit feature, so only single character identifiers become eligible as auto-implicits. See discussion on zulip and 2.

Estimated changes

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean

Modified Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

modified theorem CategoryTheory.Limits.comp_lim_obj_ext

Modified Mathlib/Computability/TuringMachine.lean

modified theorem Turing.TM1to1.tr_respects

Modified Mathlib/Data/HashMap.lean

modified def Std.RBSet.insertList

Modified Mathlib/Data/List/Range.lean

modified theorem List.range'_one

Modified Mathlib/Data/Seq/Computation.lean

modified theorem Computation.LiftRelAux_inl_inr

modified theorem Computation.LiftRelAux_inr_inl

modified theorem Computation.LiftRelAux_inr_inr

Modified Mathlib/Data/Stream/Init.lean

modified theorem Stream'.dropLast_take

Modified Mathlib/Init/Algebra/Classes.lean

Modified Mathlib/Order/Basic.lean

modified theorem PUnit.max_eq

modified theorem PUnit.min_eq

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

Modified Mathlib/SetTheory/Game/PGame.lean

Modified Mathlib/Tactic/IntervalCases.lean

Modified Mathlib/Tactic/Ring/Basic.lean

Modified Mathlib/Tactic/Ring/RingNF.lean

Modified Mathlib/Tactic/Sat/FromLRAT.lean

modified theorem Sat.Fmla.refute

modified theorem Sat.Valuation.mk_implies

Modified Mathlib/Testing/SlimCheck/Testable.lean

Modified Mathlib/Topology/MetricSpace/Gluing.lean

Modified Mathlib/Util/Syntax.lean

modified def Lean.Syntax.TSepArray.ofElems

Modified lakefile.lean