Mercurial > cpdt > repo
changeset 96:b78a55b30f4a
Move [present] section earlier
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 07 Oct 2008 21:58:45 -0400 |
parents | 7804f9d5249f |
children | e579e1e64bde |
files | src/MoreDep.v |
diffstat | 1 files changed, 16 insertions(+), 16 deletions(-) [+] |
line wrap: on
line diff
--- a/src/MoreDep.v Tue Oct 07 21:49:35 2008 -0400 +++ b/src/MoreDep.v Tue Oct 07 21:58:45 2008 -0400 @@ -398,6 +398,22 @@ Inductive rtree : nat -> Set := | RedNode' : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rtree n. +Section present. + Variable x : nat. + + Fixpoint present c n (t : rbtree c n) {struct t} : Prop := + match t with + | Leaf => False + | RedNode _ a y b => present a \/ x = y \/ present b + | BlackNode _ _ _ a y b => present a \/ x = y \/ present b + end. + + Definition rpresent n (t : rtree n) : Prop := + match t with + | RedNode' _ _ _ a y b => present a \/ x = y \/ present b + end. +End present. + Notation "{< x >}" := (existT _ _ x). Definition balance1 n (a : rtree n) (data : nat) c2 := @@ -426,22 +442,6 @@ end t2 end. -Section present. - Variable x : nat. - - Fixpoint present c n (t : rbtree c n) {struct t} : Prop := - match t with - | Leaf => False - | RedNode _ a y b => present a \/ x = y \/ present b - | BlackNode _ _ _ a y b => present a \/ x = y \/ present b - end. - - Definition rpresent n (t : rtree n) : Prop := - match t with - | RedNode' _ _ _ a y b => present a \/ x = y \/ present b - end. -End present. - Section insert. Variable x : nat.