ranjitjhala

module AVL  where
 
{-@ data Tree [ht] = Nil | Tree (x::Int) (l::Tree) (r::Tree) @-}
data Tree = Nil | Tree Int Tree Tree
 
{-@ height :: t:Tree -> {v:Int | v = ht t}  @-}
height :: Tree -> Int
height Nil          = 0
height (Tree _ l r) = (if height l > height r then 1 + height l else 1 + height r)