subtype of finset

Stream: general

[Johan Commelin]

In #2163 @Sebastien Gouezel needs to turn a finset s into a subtype. This isn't done automatically by coercions, as far as I know. I guess that for that reason he wrote s.to_set, after which the set is coerced to a type. I have written {x // x \in s} before. But that is maybe also not a very canonical form.
Is there a canonical form? If not, what do people prefer?

[Chris Hughes]

I think a coe_to_sort for finsets might be justified.