The Coq mailing list

[vsiles AT lix.polytechnique.fr]

Happy new year !

> The problem I really had was being unable to
> specify the measure function such that it can be called in snarf, the
> idea of specifying lsum on a product as opposed to currying was
> the key for me. I ended up using Function  this morning although
> Program Fixpoint works out as well.

If you really want to use a measure on the lists length, there's a little
trick I sometimes do to avoid defining complicated measure : I mark the
list with their length (transform them in vector) , compute my function
and than erase the length information.
Your function signature will look like

forall n n1 n2:nat, n=n1+n2 -> ... where list Z is replaced by vector ni Z

Writing the 'n=n1+n2' proofs in the Function can be annoying but along
with Program, it because really easy.

Cheers,
Vincent