Commit 2026-02-09 07:57 e51a743a
View on Github →chore: fix overlapping instances in meta files (#35003)
This PR is intended to satisfy the upcoming overlapping instances linter. It replaces [Monad m] [Alternative m] with [AlternativeMonad m] , which avoids overlapping on the data-carrying Applicative projection, or specializes appropriate monads like MetaM where possible.
It also fixes some other duplicated instance projections in Mathlib.Deprecated.MLList.BestFirst, even though this file is deprecated.