Mercurial > hg > Gears > GearsAgda

comparison redBlackTreeTest.agda @ 567:56a190d3c70a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lemma1 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 17 Apr 2018 09:44:06 +0900
parents d9ef8333ff79
children a5ba292e4081
comparison
equal deleted inserted replaced
566:d9ef8333ff79 567:56a190d3c70a
291 where 291 where
292 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { 292 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
293 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red 293 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red
294 } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y } ) k 294 } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y } ) k
295 ( λ t x1 → checkT x1 x ≡ True) 295 ( λ t x1 → checkT x1 x ≡ True)
296 lemma1 = {!!} 296 lemma1 with compTri k k
297 ... | tri≈ _ refl _ = checkEQ x _ refl
298 ... | tri< _ neq _ = ⊥-elim (neq refl)
299 ... | tri> _ neq _ = ⊥-elim (neq refl)