Ssreflect Users Discussion List

[Aleks Nanevski <>]

Hi everyone,

 

I was wondering what is the easiest way to define a finite type out of a sequence of elements of type T : eqType.

 

The stuff given in SeqFinType section of fintype.v is a bit too demanding, as it is asking me to first prove that T : choiceType.

 

In the previous version of ssreflect, there was a way to do this in one line (via lemma which used to be called seq_enum), but that seems to have disappeared in the new version of the libraries.

 

Thanks,

Aleks