Mercurial > hg > Gears > GearsAgda

comparison redBlackTreeTest.agda @ 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
comparison
equal deleted inserted replaced
565:ba7c5f1c2937 566:d9ef8333ff79
257 ... | tri≈ _ _ _ = True 257 ... | tri≈ _ _ _ = True
258 ... | _ = False 258 ... | _ = False
259 259
260 checkEQ : {m : Level } ( x : ℕ ) -> ( n : Node ℕ ℕ ) -> (value n ) ≡ x -> checkT {m} (Just n) x ≡ True 260 checkEQ : {m : Level } ( x : ℕ ) -> ( n : Node ℕ ℕ ) -> (value n ) ≡ x -> checkT {m} (Just n) x ≡ True
261 checkEQ x n refl with compTri (value n) x 261 checkEQ x n refl with compTri (value n) x
262 ... | tri≈ _ _ _ = refl 262 ... | tri≈ _ refl _ = refl
263 ... | _ = {!!} 263 ... | tri> _ neq gt = ⊥-elim (neq refl)
264 264 ... | tri< lt neq _ = ⊥-elim (neq refl)
265 checkT' : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m} 265
266 checkT' Nothing _ = False 266 checkEQ' : {m : Level } ( x y : ℕ ) -> ( eq : x ≡ y ) -> ( x ≟ y ) ≡ yes eq
267 checkT' (Just n) x with (value n) ≟ x 267 checkEQ' x y refl with x ≟ y
268 ... | yes _ = True 268 ... | yes refl = refl
269 ... | no _ = False 269 ... | no neq = ⊥-elim ( neq refl )
270 270
271 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ)) 271 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
272 → (k : ℕ) (x : ℕ) 272 → (k : ℕ) (x : ℕ)
273 → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x 273 → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
274 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)) 274 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))