Mercurial > hg > Gears > GearsAgda
diff redBlackTreeTest.agda @ 544:4f692df9b3db
add reference
| author | ryokka |
|---|---|
| date | Thu, 11 Jan 2018 18:54:56 +0900 |
| parents | 1595dd84fc3e |
| children | b180dc78abcf |
line wrap: on
line diff
--- a/redBlackTreeTest.agda Thu Jan 11 17:53:03 2018 +0900 +++ b/redBlackTreeTest.agda Thu Jan 11 18:54:56 2018 +0900 @@ -41,7 +41,7 @@ test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 $ \t -> putTree1 t 2 2 $ \t -> putTree1 t 3 3 - $ \t -> putTree1 t 4 4 + $ \t -> putTree1 t 4 4 $ \t -> getRedBlackTree t 4 $ \t x -> check1 x 4 ≡ True test3 = refl @@ -50,12 +50,8 @@ $ \t -> putTree1 t 2 2 $ \t -> putTree1 t 3 3 $ \t -> putTree1 t 4 4 - $ \t -> root t - --- test4 : putTree1 {_} {_} {ℕ} {ℕ} ( createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ \t -> putTree1 t 2 2 $ \t -> --- root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} ) --- test4 = refl - + $ \t -> getRedBlackTree t 4 + $ \t x -> x -- test5 : Maybe (Node ℕ ℕ) test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4 @@ -91,3 +87,19 @@ test8 : Maybe (Node ℕ ℕ) test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 $ \t -> putTree1 t 2 2 (\ t -> root t) + + +test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check1 x 1 ≡ True )) +test9 = refl + +test10 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( + \t -> putRedBlackTree t 2 2 ( + \t -> getRedBlackTree t 1 ( + \t x -> check1 x 1 ≡ True ))) +test10 = refl + +test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 + $ \t -> putRedBlackTree t 2 2 + $ \t -> putRedBlackTree t 3 3 + $ \t -> getRedBlackTree t 2 + $ \t x -> root t