--- a/RedBlackTree.agda	Sun Jan 14 17:57:38 2018 +0900
+++ b/RedBlackTree.agda	Tue Jan 16 17:14:29 2018 +0900
@@ -166,7 +166,7 @@
     insertCase1 n0 s (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
 
 ----
--- find node potition to insert or to delete, the pass will be in the stack
+-- find node potition to insert or to delete, the path will be in the stack
 -- 
 findNode : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k -> SingleLinkedStack (Node a k) -> Node a k -> t) -> t
 findNode {n} {m} {a} {k}  {t} tree s n0 n1 next = pushSingleLinkedStack s n1 (\ s -> findNode1 s n1)
@@ -215,11 +215,17 @@
 ... | equal _ = EQ
 ... | greater _ _ = GT
 
+compare2 : (x y : ℕ ) -> CompareResult {Level.zero}
+compare2 zero zero = EQ
+compare2 (suc _) zero = GT
+compare2  zero (suc _) = LT
+compare2  (suc x) (suc y) = compare2 x y
+
 
 createEmptyRedBlackTreeℕ : { m : Level } (a : Set Level.zero) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ 
 createEmptyRedBlackTreeℕ  {m} a {t} = record {
         root = Nothing
      ;  nodeStack = emptySingleLinkedStack
-     ;  compare = compareℕ
+     ;  compare = compare2
    }