equal
deleted
inserted
replaced
8 |
8 |
9 class height = |
9 class height = |
10 fixes height :: "'a \<Rightarrow> nat" |
10 fixes height :: "'a \<Rightarrow> nat" |
11 |
11 |
12 datatype 'a tree23 = |
12 datatype 'a tree23 = |
13 Leaf | |
13 Leaf ("\<langle>\<rangle>") | |
14 Node2 "'a tree23" 'a "'a tree23" | |
14 Node2 "'a tree23" 'a "'a tree23" ("\<langle>_, _, _\<rangle>") | |
15 Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23" |
15 Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23" ("\<langle>_, _, _, _, _\<rangle>") |
16 |
16 |
17 fun inorder :: "'a tree23 \<Rightarrow> 'a list" where |
17 fun inorder :: "'a tree23 \<Rightarrow> 'a list" where |
18 "inorder Leaf = []" | |
18 "inorder Leaf = []" | |
19 "inorder(Node2 l a r) = inorder l @ a # inorder r" | |
19 "inorder(Node2 l a r) = inorder l @ a # inorder r" | |
20 "inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r" |
20 "inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r" |