Mercurial > hg > Gears > GearsAgda

changeset 565:ba7c5f1c2937

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
this slightly better
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 11 Apr 2018 11:57:41 +0900
parents 40ab3d39e49d
children d9ef8333ff79
files redBlackTreeTest.agda
diffstat 1 files changed, 11 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/redBlackTreeTest.agda	Wed Apr 11 11:29:57 2018 +0900
+++ b/redBlackTreeTest.agda	Wed Apr 11 11:57:41 2018 +0900
@@ -11,7 +11,6 @@
 
 
 open import Algebra
-open import Relation.Binary
 open import Data.Nat.Properties   as NatProp
 
 open Tree
@@ -247,10 +246,10 @@
       lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
       lemma2 = refl
 
-open IsStrictTotalOrder
 
 compTri :  ( x y : ℕ ) ->  Tri  (x < y) ( x ≡ y )  ( x > y )
 compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder) 
+   where open import  Relation.Binary
 
 checkT : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool {m}
 checkT Nothing _ = False
@@ -258,6 +257,16 @@
 ...  | tri≈ _ _ _ = True
 ...  | _ = False
 
+checkEQ :  {m : Level }  ( x :  ℕ ) -> ( n : Node  ℕ ℕ ) -> (value n )  ≡ x  -> checkT {m} (Just n) x ≡ True
+checkEQ x n refl with compTri (value n)  x
+... |  tri≈ _ _ _ = refl
+... |  _ = {!!}
+
+checkT' : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool {m}
+checkT' Nothing _ = False
+checkT' (Just n) x with (value n) ≟ x
+...  | yes _ = True
+...  | no _  = False
 
 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
          → (k : ℕ) (x : ℕ)