The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Mon, Jul 16, 2007 at 11:08:54PM +0200, 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:

I don't know exactly what you want, but here is an example of a binary
tree with nodes labelled with Prop-predicates:

Inductive Tree (A:Type) : Type :=
  | Leaf : Tree A
  | Node : (A -> Prop) -> Tree A -> Tree A -> Tree A
.

-- 
Lionel