--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/bt.agda	Thu Nov 12 21:35:03 2020 +0900
@@ -0,0 +1,40 @@
+module bt where
+
+
+open import Data.Nat hiding (compare)
+open import Data.Nat.Properties as NatProp -- <-cmp
+open import Relation.Binary
+
+
+record tree (A B C : Set) : Set where
+  field
+    key : A
+    ltree : B
+    rtree : C
+
+data bst : Set where
+  bt-empty : bst
+  bt-node  : (node : tree ℕ bst bst ) → bst
+
+-- insert
+bt-insert : ℕ → bst → bst
+bt-insert n bt-empty = (bt-node (record { key = n ; ltree = bt-empty ; rtree = bt-empty }) )
+bt-insert n (bt-node (record { key = x ; ltree = l ; rtree = r }) ) with <-cmp n x
+bt-insert n (bt-node (record { key = x ; ltree = l ; rtree = r }) ) | tri≈ ¬a b ¬c = (bt-node (record { key = x ; ltree = l ; rtree = r }) )
+bt-insert n (bt-node (record { key = x ; ltree = l ; rtree = r }) ) | tri< a ¬b ¬c = (bt-node (record { key = x ; ltree = l ; rtree = (bt-insert n r) }) ) -- nの方が小さい
+bt-insert n (bt-node (record { key = x ; ltree = l ; rtree = r }) ) | tri> ¬a ¬b c = (bt-node (record { key = x ; ltree = (bt-insert n l) ; rtree = r }) ) -- nの方が大きい
+
+-- 以下test部分
+
+test-insert1 : bst
+test-insert1 = bt-insert 2 bt-empty
+
+test-insert2 : bst
+test-insert2 = bt-insert 3 test-insert1
+
+test-insert3 : bst
+test-insert3 = bt-insert 1 test-insert2
+
+test-insert4 : bst
+test-insert4 = bt-insert 4 test-insert3
+