Mercurial > hg > Members > Moririn
changeset 547:d6a2b812b056
compare2
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 14 Jan 2018 08:38:46 +0900 |
| parents | b654ce34c894 |
| children | c304869ac439 |
| files | redBlackTreeTest.agda |
| diffstat | 1 files changed, 8 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/redBlackTreeTest.agda Fri Jan 12 19:08:29 2018 +0900 +++ b/redBlackTreeTest.agda Sun Jan 14 08:38:46 2018 +0900 @@ -113,10 +113,15 @@ redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compareℕ } - +compare2 : (x y : ℕ ) -> CompareResult {Level.zero} +compare2 zero zero = EQ +compare2 (suc _) zero = GT +compare2 zero (suc _) = LT +compare2 (suc x) (suc y) = compare2 x y -putTest1Lemma1 : (k : ℕ) (x : ℕ) -> Data.Nat.compare 1 1 ≡ Data.Nat.equal 1 -putTest1Lemma1 k x = refl +putTest1Lemma1 : (k : ℕ) -> compare2 k k ≡ EQ +putTest1Lemma1 zero = refl +putTest1Lemma1 (suc k) = putTest1Lemma1 k -- begin -- Data.Nat.compare k (key (leafNode k x))