### changeset 96:b78a55b30f4a

Move [present] section earlier
author Adam Chlipala Tue, 07 Oct 2008 21:58:45 -0400 7804f9d5249f e579e1e64bde src/MoreDep.v 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.
```