Def insertUnexpander

Modification history

2022-09-08 18:38

Mathlib/Init/SetNotation.lean

chore: bump std4 09-08 (#403) …

Deleted insertUnexpander View on Github →

2022-08-22 14:24

Mathlib/Init/SetNotation.lean

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

Added insertUnexpander View on Github →