The Coq mailing list

[Nicolas Osborne <nicolas.osborne.etu AT univ-lille.fr>]

Dear Coq-Club,

I need to define a rose tree with a map instead of a list. As I don’t have any reason to care about efficiency in this context, I use FMapWeakList from the Standard Library and declare the following:

Require Import Coq.Structures.DecidableTypeEx.

Require Import Coq.FSets.FMapWeakList.

Variable T:Type.

Module M := FMapWeakList.Make(Nat_as_DT).

Inductive tree: Type := mkTree: T -> M.t tree -> tree.

Then, Coq greets me with the following error message:

      Error: Non strictly positive occurrence of "tree" in "nat -> M.t tree -> tree".

As I understand it, this means that "tree" occurs at the left of an arrow in one of the argument of the constructor (namely "M.t tree"), which is forbidden for consistency reasons.

Is there any way around ?

My first guess would be to use a list of products in the tree:

Inductive tree’: Type := mkTree’: T -> list (nat * tree’) -> tree’.

and then make sure that this list behaves like a map when writing the functions handling the modifications of the tree.

But if there is a way to use directly a map in the tree, that would be a relief.

Thanks,

Nicolas Osborne