# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1515513913 -32400
# Node ID 2d56224dbed73bcdeee80e50f3c5359118ca3f42
# Parent  7059fa504a7e40b33b225497760e6b7017853ae5
...

diff -r 7059fa504a7e -r 2d56224dbed7 RedBlackTree.agda
--- a/RedBlackTree.agda	Wed Jan 10 00:53:40 2018 +0900
+++ b/RedBlackTree.agda	Wed Jan 10 01:05:13 2018 +0900
@@ -254,9 +254,12 @@
     \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 = {!!}
+-- test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 
+--     $ \t -> putTree1 t 2 2 
+--     $ \t -> getRedBlackTree t 2 
+--     $ \t x -> check1 x 2 ≡ True  
+-- test3 = {!!}
 
+test4 : putTree1 {_} {_} {ℕ} {ℕ} ( createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $  \t -> putTree1 t 2 2  $ \t -> root t ≡ {!!} 
+test4 = refl
+