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