Mercurial > hg > Gears > GearsAgda

changeset 887:e92daa8d617b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
main part start again
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 13 May 2024 10:59:03 +0900
parents 0aac292a5e1c
children 5b6225b81409
files hoareBinaryTree1.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sun May 12 22:55:14 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon May 13 10:59:03 2024 +0900
@@ -1507,7 +1507,7 @@
  → (stack : List (bt (Color ∧ A)))
  → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
  → (exit : (r : RBI key value tree0 tree1 stack ) → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )) → t
-replaceRBTNode = ?
+replaceRBTNode key value tree0 rbi tree1 stack rbi-stack exit = ?
 
 --
 -- RBT is blanced with the stack, simply rebuild tree without rototation
@@ -1525,7 +1525,7 @@
         →  stack1 ≡ (orig ∷ [])
         →  RBI key value orig repl stack1
         → t ) → t
-rebuildRBT = ?
+rebuildRBT key value orig repl stack r bdepth-eq next exit = ?
 
 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A)