diff Paper/pic/AgdaTreeDebug.agda.replaced @ 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/pic/AgdaTreeDebug.agda.replaced	Fri Apr 13 19:47:50 2018 +0900
@@ -0,0 +1,15 @@
+test31 = putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ ) 1 1
+  $ \t @$\rightarrow$@ putTree1 t 2 2
+  $ \t @$\rightarrow$@ putTree1 t 3 3
+  $ \t @$\rightarrow$@ putTree1 t 4 4
+  $ \t @$\rightarrow$@ getRedBlackTree t 4
+  $ \t x @$\rightarrow$@ x
+
+-- Just
+-- (record
+-- { key = 4
+-- ; value = 4
+-- ; right = Nothing
+-- ; left = Nothing
+-- ; color = Red
+-- })