data BTree a = Leaf | Node (BTree a) a (BTree a) testTree : BTree String testTree = Node (Node Leaf "Jim" Leaf) "Fred" (Node (Node Leaf "Alice" Leaf) "Sheila" (Node Leaf "Bob" Leaf)) treeTagAux : (i : Int) -> BTree a -> (Int, BTree (Int, a)) treeTagAux i Leaf = (i, Leaf) treeTagAux i (Node l x r) = let (i', l') = treeTagAux i l in let x' = (i', x) in let (i'', r') = treeTagAux (i' + 1) r in (i'', Node l' x' r') treeTag : (i : Int) -> BTree a -> BTree (Int, a) treeTag i x = snd (treeTagAux i x)