Commit 2023-10-25 17:26 7f885ee9

View on Github →

feat: pretty print as ↥S instead of { x // x ∈ S } for SetLike (#7927) Adds a delaborator detecting { x // x ∈ S } where the membership uses SetLike.instMembership, since then this matches the CoeSort instance for SetLike.

Estimated changes