Mercurial > hg > Gears > GearsAgda

changeset 568:a5ba292e4081

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lemma3
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 17 Apr 2018 10:02:12 +0900
parents 56a190d3c70a
children f24a73245f36
files redBlackTreeTest.agda
diffstat 1 files changed, 5 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/redBlackTreeTest.agda	Tue Apr 17 09:44:06 2018 +0900
+++ b/redBlackTreeTest.agda	Tue Apr 17 10:02:12 2018 +0900
@@ -279,12 +279,15 @@
        putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compareT }) k x (λ t →
        GetRedBlackTree.checkNode t k (λ t₁ x1 → checkT x1 x ≡ True) (root t))
      lemma2 s with compTri k (key n1)
-     ... |  tri≈ le eq gt = lemma3
+     ... |  tri≈ le refl gt = lemma3
         where 
            lemma3 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
                key   = key n1 ; value = x ; right = right n1 ; left  = left n1 ; color = Black
                } ) ; nodeStack = s ; compare = λ x₁ y → compareT x₁ y  } ) k ( λ  t x1 → checkT x1 x  ≡ True)
-           lemma3 = {!!}
+           lemma3 with compTri k k 
+           ... | tri≈  _ refl _ = checkEQ x _ refl
+           ... | tri< _ neq _ =  ⊥-elim (neq refl)
+           ... | tri> _ neq _ =  ⊥-elim (neq refl)
      ... |  tri> le eq gt = {!!}
      ... |  tri< le eq gt = {!!}
 ...  | Nothing =  lemma1