annotate final_pre/src/AgdaTreeDebug.agda @ 7:28f900230c26

add final_pre
author ryokka
date Mon, 19 Feb 2018 23:32:24 +0900
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
7
28f900230c26 add final_pre
ryokka
parents:
diff changeset
1 test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1
28f900230c26 add final_pre
ryokka
parents:
diff changeset
2 $ \t -> putTree1 t 2 2
28f900230c26 add final_pre
ryokka
parents:
diff changeset
3 $ \t -> putTree1 t 3 3
28f900230c26 add final_pre
ryokka
parents:
diff changeset
4 $ \t -> putTree1 t 4 4
28f900230c26 add final_pre
ryokka
parents:
diff changeset
5 $ \t -> getRedBlackTree t 4
28f900230c26 add final_pre
ryokka
parents:
diff changeset
6 $ \t x -> x
28f900230c26 add final_pre
ryokka
parents:
diff changeset
7
28f900230c26 add final_pre
ryokka
parents:
diff changeset
8 -- Just
28f900230c26 add final_pre
ryokka
parents:
diff changeset
9 -- (record
28f900230c26 add final_pre
ryokka
parents:
diff changeset
10 -- { key = 4
28f900230c26 add final_pre
ryokka
parents:
diff changeset
11 -- ; value = 4
28f900230c26 add final_pre
ryokka
parents:
diff changeset
12 -- ; right = Nothing
28f900230c26 add final_pre
ryokka
parents:
diff changeset
13 -- ; left = Nothing
28f900230c26 add final_pre
ryokka
parents:
diff changeset
14 -- ; color = Red
28f900230c26 add final_pre
ryokka
parents:
diff changeset
15 -- })