26 lines
588 B
Idris
26 lines
588 B
Idris
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
|