diff Paper/src/AgdaTreeDebug.agda @ 1:bf2887cd22c1

fix Paper
author ryokka
date Fri, 13 Apr 2018 19:47:50 +0900
parents
children
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaTreeDebug.agda	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,15 @@
+test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1
+  $ \t -> putTree1 t 2 2
+  $ \t -> putTree1 t 3 3
+  $ \t -> putTree1 t 4 4
+  $ \t -> getRedBlackTree t 4
+  $ \t x -> x
+
+-- Just
+-- (record
+-- { key = 4
+-- ; value = 4
+-- ; right = Nothing
+-- ; left = Nothing
+-- ; color = Red
+-- })