The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Le 07/02/2016 21:59, Dominique Larchey-Wendling a écrit :

One way to solve this problem (this is done that way in the CoLoR

library for instance) is to have mutually inductive types for trees

and forest (aka lists of trees) and these use the Scheme command.

But the disadvantage of such a method is that a forest in

*only isomorphic* to a list of tree, and thus using

the List library to manipulate forests is uneasy. Basically,

you need to duplicate all the results from the List library.

Hello Dominique.

CoLoR does not use mutually inductive types but the same solution as yours.

See http://color.gforge.inria.fr/doc/CoLoR.Term.Varyadic.VTerm.html
for what is equivalent to your trees
and http://color.gforge.inria.fr/doc/CoLoR.Term.WithArity.ATerm.html
for the dependent version (using vectors instead of lists)

It also provides many useful functions and lemmas on lists and vectors.
See http://color.gforge.inria.fr/doc/main.html
and especially http://color.gforge.inria.fr/doc/CoLoR.Util.List.ListUtil.html
and http://color.gforge.inria.fr/doc/CoLoR.Util.Vector.VecUtil.html.

Best regards, Frédéric.