Commit 2024-07-01 13:36 2f324b49

View on Github →

chore: add exception for Data.Set.Subset to noshake.json. (#14196) We add Data.Set.Subset to the set of files ignored by the shake linter, which gives a false positive when this file is just imported for the notation.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Matroid/Map.lean

Modified Mathlib/Data/Set/Functor.lean

deleted def Set.Notation.delab_set_image_subtype

Created Mathlib/Data/Set/Notation.lean

added def Set.Notation.delab_set_image_subtype

Modified Mathlib/Data/Set/Subset.lean

Modified scripts/noshake.json