Ssreflect Users Discussion List

[Allyx FONTAINE <>]

Hi all,

Lets consider a finite type F.
I would like to define the type of finite functions which take in 
parameter an element of type F (lets call it elt)
and returns a sequence of (f elt) nat
where (f: F -> nat) .

I thought about using finfun and tuple, but I did not succeed. So I 
wonder what are the possible definitions. What do you suggest ?

Thanks for your help,
Allyx