git.iko.soy/Idris-dev
on bd2fa8d help sign in
Idris-dev/samples/tutorial/BTree.idr
22 lines 517 B history raw
1module btree
3public export
4data BTree a = Leaf
5 | Node (BTree a) a (BTree a)
7export
8insert : Ord a => a -> BTree a -> BTree a
9insert x Leaf = Node Leaf x Leaf
10insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
11 else (Node l v (insert x r))
13export
14toList : BTree a -> List a
15toList Leaf = []
16toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)
18export
19toTree : Ord a => List a -> BTree a
20toTree [] = Leaf
21toTree (x :: xs) = insert x (toTree xs)