git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/samples/TreeTag-noeff.idr
21 lines 630 B history raw
2data BTree a = Leaf
3 | Node (BTree a) a (BTree a)
5testTree : BTree String
6testTree = Node (Node Leaf "Jim" Leaf)
7 "Fred"
8 (Node (Node Leaf "Alice" Leaf)
9 "Sheila"
10 (Node Leaf "Bob" Leaf))
12treeTagAux : (i : Int) -> BTree a -> (Int, BTree (Int, a))
13treeTagAux i Leaf = (i, Leaf)
14treeTagAux i (Node l x r)
15 = let (i', l') = treeTagAux i l in
16 let x' = (i', x) in
17 let (i'', r') = treeTagAux (i' + 1) r in
18 (i'', Node l' x' r')
20treeTag : (i : Int) -> BTree a -> BTree (Int, a)
21treeTag i x = snd (treeTagAux i x)