The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

Hi Julien,

> you can try to use Function instead of Program Fixpoint. The two
> feature are not exactly equivalent. In particular, Function will give
> you a fixpoint equation for you function (aka a proof that $forall x, f
> x = body_of_f$) and an induction principle for f which will (hopefully)
> help you to reason about f. 

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?

Cheers,

Michael

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