from finset to set

Stream: general

[Johan Commelin]

I can't find a way to go from finset to set in the finset.lean file. How do I do this?

[Kenny Lau]

{x | x \in s}

[Johan Commelin]

Ok... there is no lift_to_set S thing or such?

[Kenny Lau]

not that I am aware of

[Johan Commelin]

Ok, then I'll use curly braces {-;

[Chris Hughes]

There's a has_lift instance for finset to set in data.set.finite