Mercurial > hg > Gears > GearsAgda

comparison BTree.agda @ 954:08281092430b

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 Sun, 06 Oct 2024 17:59:51 +0900
parents 24255e0dd027
children bfc7007177d0
comparison
equal deleted inserted replaced
953:24255e0dd027 954:08281092430b
553 ... | tri< a ¬b ¬c = ⊥-elim (¬b (sym keq)) 553 ... | tri< a ¬b ¬c = ⊥-elim (¬b (sym keq))
554 ... | tri≈ ¬a b ¬c = refl 554 ... | tri≈ ¬a b ¬c = refl
555 ... | tri> ¬a ¬b c = ⊥-elim (¬b (sym keq)) 555 ... | tri> ¬a ¬b c = ⊥-elim (¬b (sym keq))
556 556
557 open _∧_ 557 open _∧_
558
559
560 open _∧_
561
562 record IsNode {n : Level} {A : Set n} (t : bt A) : Set (Level.suc n) where
563 field
564 key : ℕ
565 value : A
566 left : bt A
567 right : bt A
568 t=node : t ≡ node key value left right
569
570 node→leaf∨IsNode : {n : Level} {A : Set n} → (t : bt A ) → (t ≡ leaf) ∨ IsNode t
571 node→leaf∨IsNode leaf = case1 refl
572 node→leaf∨IsNode (node key value t t₁) = case2 record { key = key ; value = value ; left = t ; right = t₁ ; t=node = refl }
573
574 IsNode→¬leaf : {n : Level} {A : Set n} (t : bt A) → IsNode t → ¬ (t ≡ leaf)
575 IsNode→¬leaf .(node key value left right) record { key = key ; value = value ; left = left ; right = right ; t=node = refl } ()
576
558 577
559 ri-tr> : {n : Level} {A : Set n} → (tree repl : bt A) → (key key₁ : ℕ) → (value : A) 578 ri-tr> : {n : Level} {A : Set n} → (tree repl : bt A) → (key key₁ : ℕ) → (value : A)
560 → replacedTree key value tree repl → key₁ < key → tr> key₁ tree → tr> key₁ repl 579 → replacedTree key value tree repl → key₁ < key → tr> key₁ tree → tr> key₁ repl
561 ri-tr> .leaf .(node key value leaf leaf) key key₁ value r-leaf a tgt = ⟪ a , ⟪ tt , tt ⟫ ⟫ 580 ri-tr> .leaf .(node key value leaf leaf) key key₁ value r-leaf a tgt = ⟪ a , ⟪ tt , tt ⟫ ⟫
562 ri-tr> .(node key _ _ _) .(node key value _ _) key key₁ value r-node a tgt = ⟪ a , ⟪ proj1 (proj2 tgt) , proj2 (proj2 tgt) ⟫ ⟫ 581 ri-tr> .(node key _ _ _) .(node key value _ _) key key₁ value r-node a tgt = ⟪ a , ⟪ proj1 (proj2 tgt) , proj2 (proj2 tgt) ⟫ ⟫