Mercurial > hg > Gears > GearsAgda

comparison redBlackTreeTest.agda @ 547:d6a2b812b056

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
compare2
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 14 Jan 2018 08:38:46 +0900
parents b654ce34c894
children c304869ac439
comparison
equal deleted inserted replaced
546:b654ce34c894 547:d6a2b812b056
111 111
112 112
113 redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ 113 redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ
114 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compareℕ } 114 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compareℕ }
115 115
116 compare2 : (x y : ℕ ) -> CompareResult {Level.zero}
117 compare2 zero zero = EQ
118 compare2 (suc _) zero = GT
119 compare2 zero (suc _) = LT
120 compare2 (suc x) (suc y) = compare2 x y
116 121
117 122 putTest1Lemma1 : (k : ℕ) -> compare2 k k ≡ EQ
118 putTest1Lemma1 : (k : ℕ) (x : ℕ) -> Data.Nat.compare 1 1 ≡ Data.Nat.equal 1 123 putTest1Lemma1 zero = refl
119 putTest1Lemma1 k x = refl 124 putTest1Lemma1 (suc k) = putTest1Lemma1 k
120 125
121 -- begin 126 -- begin
122 -- Data.Nat.compare k (key (leafNode k x)) 127 -- Data.Nat.compare k (key (leafNode k x))
123 -- ≡⟨ {!!} ⟩ 128 -- ≡⟨ {!!} ⟩
124 -- Data.Nat.equal _ 129 -- Data.Nat.equal _