Mercurial > hg > Gears > GearsAgda

changeset 566:d9ef8333ff79

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use ⊥-elim (neq refl)
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 14 Apr 2018 16:33:16 +0900
parents ba7c5f1c2937
children 56a190d3c70a
files redBlackTreeTest.agda
diffstat 1 files changed, 7 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/redBlackTreeTest.agda	Wed Apr 11 11:57:41 2018 +0900
+++ b/redBlackTreeTest.agda	Sat Apr 14 16:33:16 2018 +0900
@@ -259,14 +259,14 @@
 
 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
-... |  _ = {!!}
+... |  tri≈ _ refl _ = refl
+... |  tri> _ neq gt =  ⊥-elim (neq refl)
+... |  tri< lt neq _ =  ⊥-elim (neq refl)
 
-checkT' : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool {m}
-checkT' Nothing _ = False
-checkT' (Just n) x with (value n) ≟ x
-...  | yes _ = True
-...  | no _  = False
+checkEQ' :  {m : Level }  ( x y :  ℕ ) -> ( eq : x  ≡ y  ) -> ( x  ≟ y ) ≡ yes eq
+checkEQ' x y refl with  x  ≟ y
+... | yes refl = refl
+... | no neq = ⊥-elim ( neq refl )
 
 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
          → (k : ℕ) (x : ℕ)