Def Mathlib.Notation.unexpandExistsUnique

Modification history

2024-09-11 03:54

Mathlib/Init/Logic.lean

chore: move `ExistsUnique`, `Xor'` out of `Init.Logic` (#16691) …

Modified Mathlib.Notation.unexpandExistsUnique View on Github →

2024-04-18 05:39

Mathlib/Init/Logic.lean

feat: make `ExistsUnique` notation throw an error when used with more than one binder (#12218) …

Added Mathlib.Notation.unexpandExistsUnique View on Github →