Mercurial > hg > Gears > GearsAgda

comparison RedBlackTree.agda @ 545:b180dc78abcf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add someTest
author ryokka
date Fri, 12 Jan 2018 18:30:05 +0900
parents 1595dd84fc3e
children bc3208d510cd
comparison
equal deleted inserted replaced
544:4f692df9b3db 545:b180dc78abcf
207 search n | GT = checkNode (right n) 207 search n | GT = checkNode (right n)
208 search n | EQ = cs tree (Just n) 208 search n | EQ = cs tree (Just n)
209 209
210 open import Data.Nat hiding (compare) 210 open import Data.Nat hiding (compare)
211 211
212 compareℕ : ℕ → ℕ → CompareResult {Level.zero}
213 compareℕ x y with Data.Nat.compare x y
214 ... | less _ _ = LT
215 ... | equal _ = EQ
216 ... | greater _ _ = GT
217
218
212 createEmptyRedBlackTreeℕ : { m : Level } (a : Set Level.zero) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ 219 createEmptyRedBlackTreeℕ : { m : Level } (a : Set Level.zero) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ
213 createEmptyRedBlackTreeℕ {m} a {t} = record { 220 createEmptyRedBlackTreeℕ {m} a {t} = record {
214 root = Nothing 221 root = Nothing
215 ; nodeStack = emptySingleLinkedStack 222 ; nodeStack = emptySingleLinkedStack
216 ; compare = compare1 223 ; compare = compareℕ
217 } where 224 }
218 compare1 : ℕ → ℕ → CompareResult {Level.zero} 225
219 compare1 x y with Data.Nat.compare x y
220 ... | less _ _ = LT
221 ... | equal _ = EQ
222 ... | greater _ _ = GT
223