Mercurial > hg > Members > Moririn

changeset 699:59f80c1049e9

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, 04 Dec 2021 19:51:58 +0900
parents 28e0f7f4777d
children adb7c2101f67
files hoareBinaryTree.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Sat Dec 04 19:47:07 2021 +0900
+++ b/hoareBinaryTree.agda	Sat Dec 04 19:51:58 2021 +0900
@@ -648,6 +648,6 @@
                  → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key)  →   top-value t1 ≡ just value
               lemma7 .leaf (.leaf ∷ []) .leaf tree1 () s-single (case1 refl)
               lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ []) .(node key value t1 t2) tree1 ri s-single (case2 x) = {!!}
-              lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ x₁ ∷ s1) tree0 tree1 ri (s-right x si) found =  ?
-              lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ x₁ ∷ s1) tree0 tree1 ri (s-left x si) found =  ?
+              lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ x₁ ∷ s1) tree0 tree1 ri (s-right x si) (case2 x₂) = {!!}
+              lemma7 (node key value t1 t2) (.(node key value t1 t2) ∷ x₁ ∷ s1) tree0 tree1 ri (s-left x si) (case2 x₂) = {!!}