Commit 2024-10-09 08:43 e2b29fbc

View on Github →

chore: adaptations for lean4#5542 (#17564) In [lean4#5542](https://github.com/leanprover/lean4/pull/5542) we are deprecating inductive ... :=, structure ... :=, and class ... := for their ... where counterparts.

Estimated changes

modified structure BialgebraCat.Hom
modified structure CoalgebraCat.Hom
modified structure HopfAlgebraCat.Hom
modified structure Finset.Colex
modified structure CoolerHom
modified structure CoolerEmbedding
modified structure CoolerIso
modified structure Opposite
modified structure PerfectPairing
modified structure QuadraticModuleCat.Hom
modified structure RootPairing
modified structure RootSystem
modified structure LinearMap.IsReflective
modified structure Mathlib.Tactic.Ring.Cache
modified structure Mathlib.Tactic.AtomM.Context
modified structure Mathlib.Tactic.AtomM.State
modified structure ModelWithCorners
modified structure Cat
modified structure F
modified structure AddHom
modified structure AlgHom
modified structure DecoratedEquiv
modified structure Equiv'
modified structure FaultyManualCoercion.Equiv
modified structure FaultyUniverses.Equiv
modified structure FurtherDecoratedEquiv
modified structure ManualCoercion.Equiv
modified structure ManualInitialize.Equiv
modified structure ManualProjectionNames.Equiv
modified structure ManualUniverses.Equiv
modified structure MyFunctor
modified structure MyType
modified structure NeedsPropClass
modified structure NestedNonFullyApplied.Equiv
modified structure PartiallyAppliedStr
modified structure PrefixProjectionNames.Equiv
modified structure SetPlus
modified structure VeryPartiallyAppliedStr
modified structure ZeroHom
modified structure coercing.BSemigroup
modified structure coercing.Equiv2
modified structure coercing.FooStr
modified structure coercing.VooStr