Def unexpandExistsUnique

Modification history

2024-04-18 05:39

Mathlib/Init/Logic.lean

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

Deleted unexpandExistsUnique View on Github →

2022-10-20 15:23

Mathlib/Init/Logic.lean

chore: update lean + std4 10-20 (#483)

Modified unexpandExistsUnique View on Github →

2022-09-19 23:23

Mathlib/Init/Logic.lean

feat: add appUnexpander for ExistsUnique (#428) …

Added unexpandExistsUnique View on Github →