--- a/RedBlackTree.agda	Tue Jan 09 23:56:42 2018 +0900
+++ b/RedBlackTree.agda	Wed Jan 10 00:47:17 2018 +0900
@@ -1,7 +1,7 @@
 module RedBlackTree where
 
 open import stack
-open import Level
+open import Level hiding (zero)
 
 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
   field
@@ -210,3 +210,52 @@
         search n | LT = checkNode (left n)
         search n | GT = checkNode (right n)
         search n | EQ = cs tree (Just n)
+
+open import Data.Nat hiding (compare)
+
+createEmptyRedBlackTreeℕ : { m : Level } (a : Set Level.zero) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ ( SingleLinkedStack (Node a ℕ ) )
+createEmptyRedBlackTreeℕ  {m} a {t} = record {
+        root = Nothing
+     ;  nodeStack = createSingleLinkedStack 
+     ;  compare = compare1
+   } where
+       compare1 :  ℕ → ℕ → CompareResult {Level.zero}
+       compare1 x y with Data.Nat.compare x y
+       ... | less _ _ = LT
+       ... | equal _ = EQ
+       ... | greater _ _ = GT
+
+
+
+-- tests
+
+putTree1 : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
+putTree1 {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree)
+...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
+...                                | Just n2  = clearStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> replaceNode tree1 s n2 n1 next))
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+
+
+check1 : {m : Level } (n : Maybe (Node  ℕ ℕ)) -> ℕ -> Bool {m}
+check1 Nothing _ = False
+check1 (Just n)  x with Data.Nat.compare (value n)  x
+...  | equal _ = True
+...  | _ = False
+
+test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check1 x 1 ≡ True   ))
+test1 = refl
+
+test2 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
+    \t -> putTree1 t 2 2 (
+    \t -> getRedBlackTree t 1 (
+    \t x -> check1 x 1 ≡ True   )))
+test2 = refl
+
+test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
+    \t -> putTree1 t 2 2 (
+    \t -> getRedBlackTree t 2 (
+    \t x -> check1 x 2 ≡ True   )))
+test3 = {!!}
+