Type of finite subsets

Stream: Is there code for X?

[Antoine Chambert-Loir]

Should there be, when αis a Type, a type of finite subsets of α? With the corresponding API, starting with

def finite_set (α : Type*): Type* := { s : set α // s.finite }

Or is it OK to resort to finset (which is supposed to some computational content)?

[Eric Rodriguez]

I thought finset was meant to be the thing for this

[Anatole Dedecker]

If you are indeed interested in the type then docs#Finset is indeed the way to go, simply because this is the only bundled version we have. From what I understand, the computational content is mostly an issue for docs#Fintype vs docs#Finite.

[Yury G. Kudryashov]

docs#Finite also work for Sort _ so lemmas like docs#isOpen_iInter don't need special cases for Prop.

[Bhavik Mehta]

I would absolutely use finset for this - you don't need to be computable or have any computational content for it; I often have noncomputable finsets

[Antoine Chambert-Loir]

OK, I ended up doing that, it simplifies many things.