Zulip Chat Archive

Stream: general

Topic: subtype of finset

Johan Commelin (Mar 16 2020 at 16:39):

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 (Mar 16 2020 at 16:42):

I think a coe_to_sort for finsets might be justified.

Last updated: Aug 03 2023 at 10:10 UTC