Mercurial > hg > Papers > 2020 > ryokka-master
annotate paper/src/AgdaTreeDebugReturnNode4.agda.replaced @ 2:c7acb9211784
add code, figure. and paper fix content
| author | ryokka |
|---|---|
| date | Mon, 27 Jan 2020 20:41:36 +0900 |
| parents | |
| children |
| rev | line source |
|---|---|
| 2 | 1 test31 = putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ ) 1 1 |
| 2 $ \t @$\rightarrow$@ putTree1 t 2 2 | |
| 3 $ \t @$\rightarrow$@ putTree1 t 3 3 | |
| 4 $ \t @$\rightarrow$@ putTree1 t 4 4 | |
| 5 $ \t @$\rightarrow$@ getRedBlackTree t 4 | |
| 6 $ \t x @$\rightarrow$@ x | |
| 7 | |
| 8 -- C-c C-n test31 return | |
| 9 -- Just | |
| 10 -- (record | |
| 11 -- { key = 4 | |
| 12 -- ; value = 4 | |
| 13 -- ; right = Nothing | |
| 14 -- ; left = Nothing | |
| 15 -- ; color = Red | |
| 16 -- }) |