--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/bt_impl/find.agda.replaced	Sun Apr 24 23:13:44 2022 +0900
@@ -0,0 +1,12 @@
+find : {n m : Level} {A : Set n} {t : Set m} !$\rightarrow$! (env : Env A )
+           !$\rightarrow$! (next : (env : Env A ) !$\rightarrow$! t )
+           !$\rightarrow$! (exit : (env : Env A ) !$\rightarrow$! t ) !$\rightarrow$! t
+find env next exit = find-c (vart env) env next exit where
+    find-c : {n m : Level} {A : Set n} {t : Set m} !$\rightarrow$! (tree : bt A) !$\rightarrow$! (env : Env A )
+           !$\rightarrow$! (next : (env : Env A ) !$\rightarrow$! t )
+           !$\rightarrow$! (exit : (env : Env A ) !$\rightarrow$! t ) !$\rightarrow$! t
+    find-c leaf env next exit = exit env
+    find-c n@(node key-t value ltree rtree) env next exit with <-cmp (varn env) key-t
+    ... | tri< a !$\neg$!b !$\neg$!c = find-c ltree record env {vart = ltree ; varl = (n !$\text{::}$! (varl env))} next exit
+    ... | tri!$\approx$! !$\neg$!a b !$\neg$!c = exit record env {vart = n}
+    ... | tri> !$\neg$!a !$\neg$!b c = find-c rtree record env {vart = rtree ; varl = (n !$\text{::}$! (varl env))} next exit
\ No newline at end of file