equal
deleted
inserted
replaced
22 alist :: "('a,'v)trie \<Rightarrow> ('a * ('a,'v)trie)list"; |
22 alist :: "('a,'v)trie \<Rightarrow> ('a * ('a,'v)trie)list"; |
23 primrec "value(Trie ov al) = ov"; |
23 primrec "value(Trie ov al) = ov"; |
24 primrec "alist(Trie ov al) = al"; |
24 primrec "alist(Trie ov al) = al"; |
25 |
25 |
26 text{*\noindent |
26 text{*\noindent |
27 Association lists come with a generic lookup function: |
27 Association lists come with a generic lookup function. Its result |
|
28 involves type @{text option} because a lookup can fail: |
28 *}; |
29 *}; |
29 |
30 |
30 consts assoc :: "('key * 'val)list \<Rightarrow> 'key \<Rightarrow> 'val option"; |
31 consts assoc :: "('key * 'val)list \<Rightarrow> 'key \<Rightarrow> 'val option"; |
31 primrec "assoc [] x = None" |
32 primrec "assoc [] x = None" |
32 "assoc (p#ps) x = |
33 "assoc (p#ps) x = |