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

diff -r 2d6ccbf429ad -r 7059fa504a7e RedBlackTree.agda
--- a/RedBlackTree.agda	Wed Jan 10 00:47:17 2018 +0900
+++ b/RedBlackTree.agda	Wed Jan 10 00:53:40 2018 +0900
@@ -236,6 +236,7 @@
 
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Core
+open import Function
 
 
 check1 : {m : Level } (n : Maybe (Node  ℕ ℕ)) -> ℕ -> Bool {m}
@@ -253,9 +254,9 @@
     \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 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 
+    $ \t -> putTree1 t 2 2 
+    $ \t -> getRedBlackTree t 2 
+    $ \t x -> check1 x 2 ≡ True  
 test3 = {!!}