Mercurial > hg > Members > Moririn

changeset 534:7059fa504a7e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 10 Jan 2018 00:53:40 +0900
parents 2d6ccbf429ad
children 2d56224dbed7
files RedBlackTree.agda
diffstat 1 files changed, 5 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/RedBlackTree.agda	Wed Jan 10 00:47:17 2018 +0900
+++ b/RedBlackTree.agda	Wed Jan 10 00:53:40 2018 +0900
@@ -236,6 +236,7 @@
 
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Core
+open import Function
 
 
 check1 : {m : Level } (n : Maybe (Node  ℕ ℕ)) -> ℕ -> Bool {m}
@@ -253,9 +254,9 @@
     \t x -> check1 x 1 ≡ True   )))
 test2 = refl
 
-test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
-    \t -> putTree1 t 2 2 (
-    \t -> getRedBlackTree t 2 (
-    \t x -> check1 x 2 ≡ True   )))
+test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 
+    $ \t -> putTree1 t 2 2 
+    $ \t -> getRedBlackTree t 2 
+    $ \t x -> check1 x 2 ≡ True  
 test3 = {!!}