Commit 2022-08-22 14:24 a0d035be

View on Github →

feat: port type classes for set notation (#373)

Estimated changes

Modified Mathlib/Init/Set.lean

deleted def Set.insertUnexpander

deleted def Set.singletonUnexpander

Modified Mathlib/Init/SetNotation.lean

added def insertUnexpander

added def singletonUnexpander

Modified Mathlib/Mathport/SpecialNames.lean