The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Greetings,

Is it possible in Coq to define a search tree with nodes labeled with
predicates? By default, values in the nodes should be Set, Prop or Type.
But, I need to label nodes with (unique) predicates, for example:

Predicate A 3 4

Predicate A 3 4   Predicate C 2 6

Predicate C 8 2   Predicate B 5 4   Predicate E 3 4   Predicate D 3 7

and so on.

Thank you very much for answer,

Marko Malikoviæ
Department of Psychology
Faculty of Arts and Sciences in Rijeka
51000, Rijeka
Croatia