--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/bt_impl/replace.agda	Sun Apr 24 23:13:44 2022 +0900
@@ -0,0 +1,14 @@
+replace : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
+    → (next : Env A → t )
+    → (exit : Env A → t) → t
+replace env next exit = replace-c (varl env) env next exit where
+    replace-c : {n m : Level} {A : Set n} {t : Set m} → List (bt A) → (env : Env A )
+        → (next : Env A → t )
+        → (exit : Env A → t) → t
+    replace-c st env next exit with st
+    ... | [] = exit env
+    ... | leaf ∷ st1 = replace-c st1 env next exit
+    ... | n@(node key-t value ltree rtree) ∷ st1 with <-cmp (varn env) (key-t)
+    ... | tri< a ¬b ¬c = replace-c st1 record env{vart = (node key-t value (vart env) rtree); varl = st1} next exit
+    ... | tri≈ ¬a b ¬c = replace-c st1 record env{vart = (node key-t (varv env) ltree rtree); varl = st1} next exit
+    ... | tri> ¬a ¬b c = replace-c st1 record env{vart = (node key-t value ltree (vart env)); varl = st1} next exit
\ No newline at end of file