--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/AgdaLink.txt	Thu Jan 11 18:54:56 2018 +0900
@@ -0,0 +1,15 @@
+http://web.student.chalmers.se/groups/datx02-dtp/report.pdf
+
+
+
+https://www.google.co.jp/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&ved=0ahUKEwj-4dbpzM_YAhXDGpQKHbHXAjcQFggnMAA&url=http%3A%2F%2Fhome.iitk.ac.in%2F~shrutib%2FCS395a%2Freport.pdf&usg=AOvVaw1Qp_3vb2fO-RkdfEGT0Fun
+
+
+https://akaposi.github.io/proplogic.pdf
+
+
+
+Book:
+Verified Functional Programming in Agda
+url: https://www.amazon.co.jp/dp/B01K0MK318/ref=dp-kindle-redirect?_encoding=UTF8&btkr=1
+

--- a/redBlackTreeTest.agda	Thu Jan 11 17:53:03 2018 +0900
+++ b/redBlackTreeTest.agda	Thu Jan 11 18:54:56 2018 +0900
@@ -41,7 +41,7 @@
 test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 
     $ \t -> putTree1 t 2 2
     $ \t -> putTree1 t 3 3
-    $ \t -> putTree1 t 4 4        
+    $ \t -> putTree1 t 4 4    
     $ \t -> getRedBlackTree t 4
     $ \t x -> check1 x 4 ≡ True  
 test3 = refl
@@ -50,12 +50,8 @@
     $ \t -> putTree1 t 2 2
     $ \t -> putTree1 t 3 3
     $ \t -> putTree1 t 4 4
-    $ \t -> root t
-
--- test4 : putTree1 {_} {_} {ℕ} {ℕ} ( createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $  \t -> putTree1 t 2 2  $ \t ->
---   root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )
--- test4 = refl
-
+    $ \t -> getRedBlackTree t 4
+    $ \t x -> x
 
 -- test5 : Maybe (Node ℕ ℕ)
 test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4 
@@ -91,3 +87,19 @@
 test8 : Maybe (Node ℕ ℕ)
 test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 
     $ \t -> putTree1 t 2 2 (\ t -> root t)
+
+
+test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check1 x 1 ≡ True   ))
+test9 = refl
+
+test10 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
+    \t -> putRedBlackTree t 2 2 (
+    \t -> getRedBlackTree t 1 (
+    \t x -> check1 x 1 ≡ True   )))
+test10 = refl
+
+test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 
+    $ \t -> putRedBlackTree t 2 2
+    $ \t -> putRedBlackTree t 3 3
+    $ \t -> getRedBlackTree t 2
+    $ \t x -> root t

--- a/stack.agda	Thu Jan 11 17:53:03 2018 +0900
+++ b/stack.agda	Thu Jan 11 18:54:56 2018 +0900
@@ -50,24 +50,28 @@
 
 open Stack
 
+{--
 data Element {n : Level } (a : Set n) : Set n where
   cons : a -> Maybe (Element a) -> Element a
 
+
 datum : {n : Level } {a : Set n} -> Element a -> a
 datum (cons a _) = a
 
 next : {n : Level } {a : Set n} -> Element a -> Maybe (Element a)
 next (cons _ n) = n
+--}
 
 
-{-
 -- cannot define recrusive record definition. so use linked list with maybe.
-record Element {l : Level} (a : Set n l) : Set n (suc l) where
+record Element {l : Level} (a : Set l) : Set l where
+  inductive
+  constructor cons
   field
     datum : a  -- `data` is reserved by Agda.
     next : Maybe (Element a)
--}
 
+open Element
 
 
 record SingleLinkedStack {n : Level } (a : Set n) : Set n where