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 -- 以下省略