Mercurial > hg > Gears > GearsAgda
changeset 646:83ba41589564
.......>>>>>>>>..............>>>>>..........ZZ
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 19 Nov 2021 16:59:44 +0900 |
| parents | 6340956f143e |
| children | 7b24e17e1441 |
| files | hoareBinaryTree.agda |
| diffstat | 1 files changed, 2 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Fri Nov 19 16:47:39 2021 +0900 +++ b/hoareBinaryTree.agda Fri Nov 19 16:59:44 2021 +0900 @@ -243,7 +243,8 @@ → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t replaceP key value {tree0} {tree} repl [] Pre next exit with proj1 (proj2 Pre) ... | () -replaceP key value {tree0} {tree} repl (leaf ∷ st) Pre next exit = {!!} +replaceP key value {tree0} {tree} repl (leaf ∷ st) Pre next exit = + exit tree0 repl ⟪ proj1 Pre , subst (λ k → replacedTree key value k repl ) (si-property0 (proj1 (proj2 Pre))) (proj2 (proj2 Pre)) ⟫ replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right ) st {!!} ≤-refl ... | tri≈ ¬a b ¬c = next key value (node key value left right ) st {!!} ≤-refl where -- this case won't happen