The Coq mailing list

[Sylvain Boulme <Sylvain.Boulme AT imag.fr>]

On Wed, 19 Nov 2003, Sylvain Boulme wrote:

> With your inductive
> definition, it is seems possible to replay the paradox above (in "delta"
> definition, use "s" such "forall f. (arity s f)=O", and take a list of
> size 1 for "l").
>

> >   | Fun :
> >     (f:function) (l:(list (term s))) (H:(length l)=(arity s f)) (term s).
> >
Oops, sorry I have spoken too fast and imagine
 "((l:(list (term s))) (length l)=(arity s f)))->(term s)"
instead of what is actually written.

Your problem looks quite classical (defining mutually recursively "trees"
and "forests" of terms). So you should have a look in contribs. There are
maybe standard solutions.

S.
______________________________________________________________________
BOULME Sylvain, ENSIMAG-LSR     | e-mail :      
Sylvain.Boulme AT imag.fr
BP-72  38402 St-MARTIN D'HERES  | tel : 04-76-82-72-89, 06-86-24-41-70