Mercurial > hg > Gears > GearsAgda

changeset 582:1a5dd71199f1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 02 Nov 2019 19:33:37 +0900
parents 09e9e8fd7568
children d18df2e6135d
files hoareRedBlackTree.agda
diffstat 1 files changed, 4 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/hoareRedBlackTree.agda	Sat Nov 02 19:23:10 2019 +0900
+++ b/hoareRedBlackTree.agda	Sat Nov 02 19:33:37 2019 +0900
@@ -131,11 +131,12 @@
 
 
 findNode1h : {n m  : Level } {a : Set n} {t : Set m}  → (tree : RedBlackTree {n} a )  → (Node a )
-     → ( FindNodeInvariant (nodeStack tree)  tree)  → ((new : RedBlackTree {n} a) →  FindNodeInvariant (nodeStack new) tree → t ) → t
-findNode1h {n} {m} {a} {t} tree n0 prev next = findNode2h (root tree) (nodeStack tree) prev
+     → ((new : RedBlackTree {n} a) →  FindNodeInvariant (nodeStack new) tree → t ) 
+     → ( FindNodeInvariant (nodeStack tree)  tree) → t
+findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) prev
   module FindNodeH where
     findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s tree  → t
-    findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } {!!} -- ( fni-Last ? )
+    findNode2h nothing st prev = next record { root = nothing ; nodeStack = st }  {!!}
     findNode2h (just x) st prev with <-cmp (key n0) (key x)
     ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? )
     ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 tree {!!} {!!}) )