Mercurial > hg > Members > Moririn
changeset 567:56a190d3c70a
lemma1 done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 17 Apr 2018 09:44:06 +0900 |
| parents | d9ef8333ff79 |
| children | a5ba292e4081 |
| files | redBlackTreeTest.agda |
| diffstat | 1 files changed, 4 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/redBlackTreeTest.agda Sat Apr 14 16:33:16 2018 +0900 +++ b/redBlackTreeTest.agda Tue Apr 17 09:44:06 2018 +0900 @@ -293,4 +293,7 @@ key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y } ) k ( λ t x1 → checkT x1 x ≡ True) - lemma1 = {!!} + lemma1 with compTri k k + ... | tri≈ _ refl _ = checkEQ x _ refl + ... | tri< _ neq _ = ⊥-elim (neq refl) + ... | tri> _ neq _ = ⊥-elim (neq refl)