# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1572690817 -32400
# Node ID 1a5dd71199f113a4721072664e6a5207fa2340ab
# Parent  09e9e8fd7568e137d2ed731db9e06466c1846e66
...

diff -r 09e9e8fd7568 -r 1a5dd71199f1 hoareRedBlackTree.agda
--- a/hoareRedBlackTree.agda	Sat Nov 02 19:23:10 2019 +0900
+++ b/hoareRedBlackTree.agda	Sat Nov 02 19:33:37 2019 +0900
@@ -131,11 +131,12 @@
 
 
 findNode1h : {n m  : Level } {a : Set n} {t : Set m}  → (tree : RedBlackTree {n} a )  → (Node a )
-     → ( FindNodeInvariant (nodeStack tree)  tree)  → ((new : RedBlackTree {n} a) →  FindNodeInvariant (nodeStack new) tree → t ) → t
-findNode1h {n} {m} {a} {t} tree n0 prev next = findNode2h (root tree) (nodeStack tree) prev
+     → ((new : RedBlackTree {n} a) →  FindNodeInvariant (nodeStack new) tree → t ) 
+     → ( FindNodeInvariant (nodeStack tree)  tree) → t
+findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) prev
   module FindNodeH where
     findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s tree  → t
-    findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } {!!} -- ( fni-Last ? )
+    findNode2h nothing st prev = next record { root = nothing ; nodeStack = st }  {!!}
     findNode2h (just x) st prev with <-cmp (key n0) (key x)
     ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? )
     ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 tree {!!} {!!}) )