The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Nothing's impossible but certainly, it won't happen overnight :) In
the meanwhile, you might be interested in this work by Arthur
Charguéraud :
http://www.chargueraud.org/arthur/research/2009/fixwf/
In particular, his fixpoint library has some support for
mutually-recursive functions.

HTH,

Stéphane L.

On Tue, May 26, 2009 at 4:59 PM, Guilhem Moulin
<guilhem.moulin AT ens-lyon.org>
 wrote:
> Argh
> And knowing the implementation of the "Function" keyword, do you think
> at first glance if it is possible to modify it in that way?
>
> Thanks anyway,
> Guilhem.
>
> On Tue, 26 May 2009 at 16:44:36 +0200, Yves Bertot wrote:
>> As far as I know, mutual recursion is only provided for structural
>> recursive functions in the "Function"
>> command.  I don't know of any tool in Coq supporting combined mutual
>> recursion and well-founded
>> induction.
>>
>> Yves
>
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v1.4.9 (GNU/Linux)
>
> iEYEARECAAYFAkocA+sACgkQ42JSn70VGn1C+wCfTzbx8zYlevQq1ngjT8bgXqUW
> iPIAn2R3DQJq8gkRYfartZ6X10uq0KSh
> =LEpF
> -----END PGP SIGNATURE-----
>
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06