Sep typeclass does not work

Stream: lean4

[Asei Inoue]

Sep typeclass docstring says this make us enable to use set notation { x : T | p x }. But actually Sep does not have an implementation of syntax…

[Asei Inoue]

why? under construction?

[Yury G. Kudryashov]

docs#Sep docstring says {x ∈ s | p x}, not {x : T | p x}. It works, at least with Mathlib.

[Yury G. Kudryashov]

It looks like Mathlib implements this syntax without using Sep class.

[Yaël Dillies]

Yes, my understanding is that Sep became vestigial during the port