The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

Hi Julien,

> Is it possible to use Function to write functions that are not directly 
> structurally recursive? For example, a function that takes a list whose 
> length decreases in recursive calls, without necessarily being a subterm 
> of the original list?

Sorry for this redundant question, I didn't realise that the "measure" 
keyword also works for Function, and this is all covered in the relevant 
documentation :)

Best regards,

Michael

--
Print XML with Prince!
http://www.princexml.com