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
|