Mercurial > hg > Gears > GearsAgda

changeset 536:2d86242ee853

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:10:35 +0900
parents 2d56224dbed7
children fffeaf0b0024
files RedBlackTree.agda
diffstat 1 files changed, 2 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/RedBlackTree.agda	Wed Jan 10 01:05:13 2018 +0900
+++ b/RedBlackTree.agda	Wed Jan 10 01:10:35 2018 +0900
@@ -260,6 +260,7 @@
 --     $ \t x -> check1 x 2 ≡ True  
 -- test3 = {!!}
 
-test4 : putTree1 {_} {_} {ℕ} {ℕ} ( createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $  \t -> putTree1 t 2 2  $ \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 = Nothing ; right = Just ( record { key = 2 ; value = 2 } ) } )
 test4 = refl