Mercurial > hg > Members > Moririn

comparison redBlackTreeTest.agda @ 542:ee65e69c9b62

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
puttree1 act
author ryokka
date Thu, 11 Jan 2018 17:38:13 +0900
parents 429ece770187
children 1595dd84fc3e
comparison
equal deleted inserted replaced
541:429ece770187 542:ee65e69c9b62
36 \t -> putTree1 t 2 2 ( 36 \t -> putTree1 t 2 2 (
37 \t -> getRedBlackTree t 1 ( 37 \t -> getRedBlackTree t 1 (
38 \t x -> check1 x 1 ≡ True ))) 38 \t x -> check1 x 1 ≡ True )))
39 test2 = refl 39 test2 = refl
40 40
41 test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 41 test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1
42 $ \t -> putTree1 t 2 2 42 $ \t -> putTree1 t 2 2
43 $ \t -> getRedBlackTree t 2 43 $ \t -> putTree1 t 3 3
44 $ \t x -> check1 x 2 ≡ True 44 $ \t -> putTree1 t 4 4
45 test3 = {!!} -- refl 45 $ \t -> getRedBlackTree t 4
46 $ \t x -> check1 x 4 ≡ True
47 test3 = refl
48
49 test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1
50 $ \t -> putTree1 t 2 2
51 $ \t -> putTree1 t 3 3
52 $ \t -> putTree1 t 4 4
53 $ \t -> root t
46 54
47 -- test4 : putTree1 {_} {_} {ℕ} {ℕ} ( createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ \t -> putTree1 t 2 2 $ \t -> 55 -- test4 : putTree1 {_} {_} {ℕ} {ℕ} ( createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ \t -> putTree1 t 2 2 $ \t ->
48 -- root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} ) 56 -- root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )
49 -- test4 = refl 57 -- test4 = refl
50 58