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