Mercurial > hg > Papers > 2018 > ryokka-sigos
comparison Paper/src/AgdaTreeImpl.agda @ 3:576637483425
fix section, source code,etc
author | ryokka |
---|---|
date | Thu, 19 Apr 2018 20:28:12 +0900 |
parents | bf2887cd22c1 |
children | 4312a27022d1 |
comparison
equal
deleted
inserted
replaced
2:43e263faf88b | 3:576637483425 |
---|---|
28 putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t | 28 putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t |
29 putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree) | 29 putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree) |
30 ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) | 30 ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) |
31 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)) | 31 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)) |
32 | 32 |
33 -- 以下省略 |