The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I would like to write a recursive function that takes 3 arguments: an 
element index (0-based), a count of elements, and a heterogeneous tuple 
containing (usually) that many elements - and have it return the indexed 
element of the tuple if it exists.  If the tuple doesn't contain the 
right number of elements, I don't care what the function does, and I 
don't want to provide a proof that the tuple contains the right number 
of elements.  The index < count - and if not, then I don't care what the 
function does.

Notes: the tuple arg will be strictly right-associated.  If count =1, 
then the third arg is just an arbitrarily-typed singleton, and is the 
result itself.  If count>1, then the last element is the snd of the last 
pair, while all previous elements are the fst of some pair.

I know how to do this when the container is homogeneous, as with lists 
or vectors - but not with hetero tuples.  I don't even know how to write 
the type of the function in this case.

Also, I think I may have seen the solution to this somewhere - but don't 
remember where...  Was it in CPDT somewhere?

Any clues on how to write this function?

Thanks,
-- Jonathan