module HomeworkSeven
%default total

data Tree = Node String Tree Tree | Leaf

data Height : Tree -> Nat -> Type where
  HLeaf : Height Leaf 1
  HNode : Height t1 n1 -> Height t2 n2 -> Height (Node s t1 t2) (S (max n1 n2))

e1 : Height (Node "a" Leaf Leaf) 2
e1 = HNode HLeaf HLeaf

e2 : Height (Node "b" Leaf (Node "a" Leaf Leaf)) 3
e2 = HNode HLeaf e1

e3 : Height (Node "c" (Node "b" Leaf (Node "a" Leaf Leaf)) Leaf) 4
e3 = HNode e2 HLeaf

--
-- -------------
--   Leaf ^ 1
--
-- t1 ^ n1  t2 ^ n2  n = 1 + max(n1,n2)
-- ------------------------------------
--         Tree s t1 t2 ^ n