Mercurial > hg > Gears > GearsAgda
changeset 699:59f80c1049e9
...
| 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₂) = {!!}