The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Perhaps someone else understands your explanation or example, but I 
don't.  It would probably be better to give "pseudo-Coq" code; that is, 
make it look as much like a valid Coq session as possible, but feeling 
free to cut corners where necessary (like when something won't really 
type-check).

Marko Malikoviæ wrote:
> 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.