Commit 2022-09-19 23:23 0d2b4d6e

View on Github →

feat: add appUnexpander for ExistsUnique (#428) Follows the same pattern as the unexpander for Exists: https://github.com/leanprover/lean4/blob/ad0f8d32584496330c15055c5e1c3dc795bb8679/src/Init/NotationExtra.lean#L170-L174 Closes #421.

Estimated changes

Modified Mathlib/Init/Logic.lean

added def unexpandExistsUnique