Mercurial > hg > Members > soto > experimental
diff bt.agda @ 5:5b56077a1862
add continuation insert at LLRBTree
| author | soto |
|---|---|
| date | Mon, 23 Nov 2020 15:42:10 +0900 |
| parents | fb1b3d066f63 |
| children |
line wrap: on
line diff
--- a/bt.agda Sat Nov 21 14:50:05 2020 +0900 +++ b/bt.agda Mon Nov 23 15:42:10 2020 +0900 @@ -158,7 +158,7 @@ rbt-insert : bst → ℕ → List bst → bst rbt-insert bt-empty n stack = merge-tree (bt-node (record { key = record { coler = red ; number = n }; ltree = bt-empty; rtree = bt-empty }) ) stack --- ( bt-node (record { key = record { coler = red ; number = n }; ltree = bt-empty; rtree = bt-empty }) ) -- mergeに遷移する +-- ( bt-node (record { key = record { coler = red ; nu mber = n }; ltree = bt-empty; rtree = bt-empty }) ) -- mergeに遷移する rbt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack with <-cmp x n rbt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack | tri≈ ¬a b ¬c = (bt-node (record { key = record { coler = y ; number = x }; ltree = l; rtree = r }) )