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.

Estimated changes