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 = {!!}
 -}
+
+