equal
deleted
inserted
replaced
16 TF_of_list :: "i=>i" |
16 TF_of_list :: "i=>i" |
17 |
17 |
18 tree, forest, tree_forest :: "i=>i" |
18 tree, forest, tree_forest :: "i=>i" |
19 |
19 |
20 datatype |
20 datatype |
21 "tree(A)" = "Tcons" ("a: A", "f: forest(A)") |
21 "tree(A)" = Tcons ("a: A", "f: forest(A)") |
22 and |
22 and |
23 "forest(A)" = "Fnil" | "Fcons" ("t: tree(A)", "f: forest(A)") |
23 "forest(A)" = Fnil | Fcons ("t: tree(A)", "f: forest(A)") |
24 |
24 |
25 rules |
25 rules |
26 TF_rec_def |
26 TF_rec_def |
27 "TF_rec(z,b,c,d) == Vrec(z, \ |
27 "TF_rec(z,b,c,d) == Vrec(z, \ |
28 \ %z r. tree_forest_case(%x f. b(x, f, r`f), \ |
28 \ %z r. tree_forest_case(%x f. b(x, f, r`f), \ |