equal
deleted
inserted
replaced
7 imports Main |
7 imports Main |
8 begin |
8 begin |
9 |
9 |
10 datatype 'a tree = |
10 datatype 'a tree = |
11 Leaf ("\<langle>\<rangle>") | |
11 Leaf ("\<langle>\<rangle>") | |
12 Node "'a tree" (root_val: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)") |
12 Node "'a tree" (root: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)") |
13 datatype_compat tree |
13 datatype_compat tree |
|
14 |
|
15 primrec left :: "'a tree \<Rightarrow> 'a tree" where |
|
16 "left (Node l v r) = l" | |
|
17 "left Leaf = Leaf" |
|
18 |
|
19 primrec right :: "'a tree \<Rightarrow> 'a tree" where |
|
20 "right (Node l v r) = r" | |
|
21 "right Leaf = Leaf" |
14 |
22 |
15 text\<open>Counting the number of leaves rather than nodes:\<close> |
23 text\<open>Counting the number of leaves rather than nodes:\<close> |
16 |
24 |
17 fun size1 :: "'a tree \<Rightarrow> nat" where |
25 fun size1 :: "'a tree \<Rightarrow> nat" where |
18 "size1 \<langle>\<rangle> = 1" | |
26 "size1 \<langle>\<rangle> = 1" | |