Fset of a fintype

[Nemeras]

Hi, Is there a reason that a {fset T} with T a fintype isn't considered a fintype ?

[CohenCyril]

Is there a reason that a {fset T} with T a fintype isn't considered a fintype ?

What do you mean "isn't considered a fintype" ?

[strub]

I would expect this to work:

From mathcomp Require Import all_ssreflect finmap.

Parameter T : finType.

Check [finType of {fset T}].

[CohenCyril]

Ah ok, sure, no reason except I forgot ... so please submit a PR if you wish.