The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

It has been a long time I didn't talked about records ;)

I used to be sad of the fact that records are not allowed to appear in
recursive structures, and already tried to modify the coq code, but it
was messing with classes.

At that time I was wondering it had some sense to mix classes and usual
records, so that we could have records mixed with recursives structures.

I still don't have a good answer to this question, but imagine you are
in this situation:
>>>
Inductive tree: Set :=
| Leaf: tree
| Branch: forest -> tree
with forest: Set :=
| Edge: forest
| Undergrowth: tree -> forest -> forest.

Class Eq (T: Set): Set :=
{ eq_: forall (t1 t2: T), {t1=t2}+{t1<>t2}
}.

Instance eqtree: Eq tree
with eqforest: Eq forest.
<<<
This start of code won't be accepted, due to coq syntax.
But clearly "eqtree" could make use of "eqforest" and vice-versa.

So at this time, the only way I know is to use Fixpoint (or Induction
Scheme, but I am not very found of it) and then use it for "eqtree" and
for "eqforest", which is not very elegant (IMO).

I didn't sent a feature request since:
1) I was lazy
2) I guess (even if I don't remember of it), that it has already been
discussed

Will there be (or is there already) an elegant workaround for this?