equal
deleted
inserted
replaced
3 section \<open>Unbalanced Tree Implementation of Map\<close> |
3 section \<open>Unbalanced Tree Implementation of Map\<close> |
4 |
4 |
5 theory Tree_Map |
5 theory Tree_Map |
6 imports |
6 imports |
7 Tree_Set |
7 Tree_Set |
8 Map_by_Ordered |
8 Map_Specs |
9 begin |
9 begin |
10 |
10 |
11 fun lookup :: "('a::linorder*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where |
11 fun lookup :: "('a::linorder*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where |
12 "lookup Leaf x = None" | |
12 "lookup Leaf x = None" | |
13 "lookup (Node l (a,b) r) x = |
13 "lookup (Node l (a,b) r) x = |