Mercurial > hg > Gears > GearsAgda
diff RedBlackTree.agda @ 541:429ece770187
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 11 Jan 2018 15:16:44 +0900 |
| parents | 6a4830c5a514 |
| children | ee65e69c9b62 |
line wrap: on
line diff
--- a/RedBlackTree.agda Thu Jan 11 11:55:22 2018 +0900 +++ b/RedBlackTree.agda Thu Jan 11 15:16:44 2018 +0900 @@ -60,8 +60,8 @@ replaceNode1 s Nothing = next ( record tree { root = Just (record n0 { color = Black}) } ) replaceNode1 s (Just n1) with compare tree (key n1) (key n0) ... | EQ = next tree - ... | GT = replaceNode tree s ( record n1 { right = Just n0 } ) next - ... | LT = replaceNode tree s ( record n1 { left = Just n0 } ) next + ... | GT = replaceNode tree s ( record n1 { left = Just n0 } ) next + ... | LT = replaceNode tree s ( record n1 { right = Just n0 } ) next rotateRight : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Maybe (Node a k) -> Maybe (Node a k) ->