doc-src/Tutorial/Datatype/update
author paulson
Fri, 23 Jun 2000 10:33:11 +0200
changeset 9109 0085c32a533b
parent 5851 15ce4c1c8313
permissions -rw-r--r--
sum_below f n -> setsum f (lessThan n)
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))"