The Coq mailing list

[Ben Lippmeier <benl AT ouroborus.net>]

> 
>>> I do not understand what you mean by "in-place".
>> For example stuff like
>> Inductive tree : Set :=
>> | Leaf: something -> tree
>> | Node: treeChildren -> something -> tree
>> with treeChildren : Set :=
>> | empty: treeChildren
>> | Cons: tree -> treeChildren ->treeChildren
>> 
>> If I understand correctly is common wisdom in the coq community that
>> the mutually recursive definition defined over is easier to manage
>> then an "equivalent"
>> 
>> Inductive tree : Set :=
>> | Leaf: something -> tree
>> | Node: list tree -> something -> tree
> 
> Yes, that is often the case.
> But in both cases you will have pros and cons.
> Some people tend to prefer to use first solution and others to use the
> second.

The second definition of 'tree' above is using "indirect mutual recursion" -- 
the recursive use of 'tree' in 'Node' is via another type 'list' that isn't 
defined in the same recursive group. You end up with the same problem when 
trying to define language grammars that contain lists of case alternatives.

It's not too hard to deal with once you know how to define the induction 
principles. There is an example for a simple lambda language with 'case' in 
the Iron Lambda collection here: 

http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SimpleData/ExpBase.v

and uses of it here:
http://code.ouroborus.net/iron/iron-head/done/Iron/Language/SimpleData/ExpLift.v

Ben.