Mercurial > hg > Papers > 2021 > soto-prosym
comparison Paper/src/AgdaTreeTest.agda.replaced @ 5:339fb67b4375
INIT rbt.agda
author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 07 Nov 2021 00:51:16 +0900 |
parents | c59202657321 |
children |
comparison
equal
deleted
inserted
replaced
4:72667e8198e2 | 5:339fb67b4375 |
---|---|
1 test31 = putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ ) 1 1 | 1 test31 = putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! ) 1 1 |
2 $ \t @$\rightarrow$@ putTree1 t 2 2 | 2 $ \t !$\rightarrow$! putTree1 t 2 2 |
3 $ \t @$\rightarrow$@ putTree1 t 3 3 | 3 $ \t !$\rightarrow$! putTree1 t 3 3 |
4 $ \t @$\rightarrow$@ putTree1 t 4 4 | 4 $ \t !$\rightarrow$! putTree1 t 4 4 |
5 $ \t @$\rightarrow$@ getRedBlackTree t 4 | 5 $ \t !$\rightarrow$! getRedBlackTree t 4 |
6 $ \t x @$\rightarrow$@ x | 6 $ \t x !$\rightarrow$! x |