Mercurial > hg > Gears > GearsAgda

changeset 535:2d56224dbed7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 10 Jan 2018 01:05:13 +0900
parents 7059fa504a7e
children 2d86242ee853
files RedBlackTree.agda
diffstat 1 files changed, 8 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- 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
+