Mercurial > hg > Gears > GearsAgda
diff work.agda @ 786:12e19644535e
test
author | Moririn < Moririn@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 02 Oct 2023 18:44:21 +0900 |
parents | dca93aef5e36 |
children | 6f27c2c18035 |
line wrap: on
line diff
--- a/work.agda Mon Aug 21 19:29:26 2023 +0900 +++ b/work.agda Mon Oct 02 18:44:21 2023 +0900 @@ -163,7 +163,7 @@ black-depth (node key ⟪ Black , value ⟫ t t₁) = suc (black-depth t ⊔ black-depth t₁ ) data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where - rb-leaf : RBtreeInvariant leaf + rb-leaf : RBtreeInvariant leaf rb-single : (key : ℕ) → (value : A) → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf leaf) rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → black-depth t ≡ black-depth t₁ @@ -354,3 +354,5 @@ rbi-case1 {n} {A} {key} (node key1 ⟪ Black , value1 ⟫ l r) leaf rbip rbir (node key3 ⟪ Red , val3 ⟫ la ra) (node key4-- ⟪ Red , val4 ⟫ lb rb) pa li ri = {!!} -} + +