Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Hi Arthur,

Arthur Azevedo de Amorim <> writes:

> Ah, that does help! I guess I was missing the /(enum _) part.

You can also do "rewrite /enum_mem".

> Still, it's a bit unfortunate to have to have to unfold so much before
> being able to unlock Finite.enum. It'd be nice if there were an easier
> way...

Surely there is, I have no clue on how fintype is supposed to work.

[I tried to do the same you are trying to do some time back, but for now
I've settled in using all, allP, elim: (enum P) and friends....]

Best,
Emilio