diff Paper/src/AgdaTreeDebugReturnNode4.agda.replaced @ 0:14a0e409d574

ADD fast commit
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 24 Apr 2022 23:13:44 +0900
parents
children
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/AgdaTreeDebugReturnNode4.agda.replaced	Sun Apr 24 23:13:44 2022 +0900
@@ -0,0 +1,16 @@
+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
+
+-- C-c C-n test31 return
+  -- Just
+  -- (record
+  -- { key = 4
+  -- ; value = 4
+  -- ; right = Nothing
+  -- ; left = Nothing
+  -- ; color = Red
+  -- })