The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Adam Koprowski wrote:
> On Mon, Mar 16, 2009 at 17:28, dimitrisg7 <dvekris AT hotmail.com 
> <mailto:dvekris AT hotmail.com>> wrote:
>
>     [...] I would be happy if I could have something like:
>
>     Inductive data_prop ...
>     ...
>     ...
>     with Fixpoint func (data_prop).
>
>  That's a very good question indeed.  I was wondering about that 
> myself. In my work I'll also need an inductively defined tree-like 
> data-structure whose component's type depends on the subtree, hence 
> I'd like to compute it with a (mutually recursive) Fixpoint function.

This is called "inductive-recursive definitions" and is supported 
natively by Agda but not Coq.