| changeset 15338 | 08519594b0e4 |
| parent 15337 | 628d87767434 |
| child 15339 | a7b603bbc1e6 |
| 15337:628d87767434 | 15338:08519594b0e4 |
|---|---|
1 consts update :: ('a,'v)trie => 'a list => 'v => ('a,'v)trie |
|
2 |
|
3 primrec |
|
4 "update t [] v = Trie (Some v) (alist t)" |
|
5 "update t (a#as) v = (let tt = (case assoc (alist t) a of |
|
6 None => Trie None [] | Some at => at) |
|
7 in Trie (value t) ((a,update tt as v)#alist t))" |