10 lines
310 B
Coq
10 lines
310 B
Coq
Inductive colour: Set := Red | Black.
|
|
|
|
(* colour of root, black height *)
|
|
Inductive tree {A:Type}: colour -> nat -> Type :=
|
|
| Empty: tree Black 0
|
|
| RNode: forall n:nat,
|
|
A -> tree Black n -> tree Black n -> tree Red n
|
|
| BNode: forall (n:nat) (c1 c2:colour),
|
|
A -> tree c1 n -> tree c2 n -> tree Black n.
|