--- a/RedBlackTree.agda	Wed Jan 17 17:31:41 2018 +0900
+++ b/RedBlackTree.agda	Wed Jan 17 18:28:25 2018 +0900
@@ -59,7 +59,7 @@
           replaceNode1 : SingleLinkedStack (Node a k) -> Maybe ( Node a k ) -> t 
           replaceNode1 s Nothing = next ( record tree { root = Just (record n0 { color = Black}) } )
           replaceNode1 s (Just n1) with compare tree (key n1) (key n0)
-          ... | EQ =  next tree
+          ... | EQ =  replaceNode tree s ( record n1 { value = value n0 ; left = left n0 ; right = right n0 } ) next
           ... | GT =  replaceNode tree s ( record n1 { left = Just n0 } ) next
           ... | LT =  replaceNode tree s ( record n1 { right = Just n0 } ) next
 
@@ -176,7 +176,7 @@
     findNode2 s (Just n) = findNode tree s n0 n next
     findNode1 : SingleLinkedStack (Node a k) -> (Node a k)  -> t
     findNode1 s n1 with (compare tree (key n0) (key n1))
-    ...                                | EQ = popSingleLinkedStack s ( \s _ -> next tree s (record n1 { key = key n1 ; value = value n1 } ) )
+    ...                                | EQ = popSingleLinkedStack s ( \s _ -> next tree s (record n1 { key = key n1 ; value = value n0 } ) )
     ...                                | GT = findNode2 s (right n1)
     ...                                | LT = findNode2 s (left n1)
 
@@ -197,7 +197,7 @@
 
 getRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> (RedBlackTree {n} {m} {t} a k -> (Maybe (Node a k)) -> t) -> t
 getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree)
-  where
+  module GetRedBlackTree where                     -- http://agda.readthedocs.io/en/v2.5.2/language/let-and-where.html
     search : Node a k -> t
     checkNode : Maybe (Node a k) -> t
     checkNode Nothing = cs tree Nothing