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" ("value": 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)") |
13 datatype_compat tree |
13 datatype_compat tree |
14 |
14 |
15 primrec left :: "'a tree \<Rightarrow> 'a tree" where |
15 primrec left :: "'a tree \<Rightarrow> 'a tree" where |
16 "left (Node l v r) = l" | |
16 "left (Node l v r) = l" | |
17 "left Leaf = Leaf" |
17 "left Leaf = Leaf" |