Mercurial > hg > Members > Moririn

changeset 546:b654ce34c894

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add putTest1Lemma1, putTest1
author ryokka
date Fri, 12 Jan 2018 19:08:29 +0900
parents b180dc78abcf
children d6a2b812b056
files redBlackTreeTest.agda
diffstat 1 files changed, 19 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/redBlackTreeTest.agda	Fri Jan 12 18:30:05 2018 +0900
+++ b/redBlackTreeTest.agda	Fri Jan 12 19:08:29 2018 +0900
@@ -113,11 +113,29 @@
 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ℕ }
 
+
+
+putTest1Lemma1 : (k : ℕ) (x : ℕ) -> Data.Nat.compare 1 1 ≡ Data.Nat.equal 1
+putTest1Lemma1 k x = refl
+
+-- begin
+--     Data.Nat.compare k (key (leafNode k x)) 
+--   ≡⟨ {!!} ⟩
+--     Data.Nat.equal _
+--   ∎
+
+
 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
          -> (k : ℕ) (x : ℕ) 
          -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
          (\ t -> getRedBlackTree t k (\ t x1 -> check1 x1 x  ≡ True)) 
-putTest1 n k x = {!!}
+putTest1 n k x with n
+...  | Just n1 = {!!}
+...  | Nothing = {!!}
+
+
+-- with Data.Nat.compare k (key (leafNode k x))
+-- ...            | Data.Nat.equal _ = ?
 
 -- begin
 --     ?