set to finset

Stream: general

[Antoine Labelle]

I'm trying to convert a set inside a fintype to a finset, but set.to_finset does not work:

import data.fintype.basic

def test (ι : Type) [fintype ι] (s : set ι) : finset ι := s.to_finset  --lean does not accept that

What is the right way to do that?

[Eric Wieser]

The error message you get is not "Lean does not accept that", right?

[Antoine Labelle]

The error message is

failed to synthesize type class instance for
ι : Type,
_inst_1 : fintype ι,
s : set ι
⊢ fintype ↥s

[Eric Wieser]

Does [decidable_pred (\mem s)] fix it?

[Antoine Labelle]

It does, thanks

[Eric Wieser]

The explanation is that the algorithm is to iterate all of ι and keep the ones that are in s; but that means you need a way to test if they're in s!

[Kevin Buzzard]

One way to debug this kind of question is to Open Classical, see if that fixes it, and then use #synth to find out what it found and then deduce why it didn't find it before

[Anne Baanen]

Or in the old-fashioned, less-uppercase Lean 3 way: open_locale classical :)