doc-src/Tutorial/Datatype/update
author wenzelm
Sat, 01 Jul 2000 19:49:20 +0200
changeset 9226 cbe6144f0f15
parent 5851 15ce4c1c8313
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5851
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     1
consts update :: ('a,'v)trie => 'a list => 'v => ('a,'v)trie
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     2
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     3
primrec
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     4
  "update t []     v = Trie (Some v) (alist t)"
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     5
  "update t (a#as) v = (let tt = (case assoc (alist t) a of
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     6
                                    None => Trie None [] | Some at => at)
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     7
                        in Trie (value t) ((a,update tt as v)#alist t))"