Mercurial > hg > Papers > 2023 > soto-master
annotate Paper/src/AgdaTreeDebugReturnNode4.agda @ 1:a72446879486
Init paper
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 12 Jan 2023 20:28:50 +0900 |
| parents | |
| children |
| rev | line source |
|---|---|
| 1 | 1 test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 |
| 2 $ \t -> putTree1 t 2 2 | |
| 3 $ \t -> putTree1 t 3 3 | |
| 4 $ \t -> putTree1 t 4 4 | |
| 5 $ \t -> getRedBlackTree t 4 | |
| 6 $ \t x -> 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 -- }) |