Go backward to Heterogeneous Arrays Go up to Top Go forward to Heterogeneous Arrays

Heterogeneous Arrays

update-value: Nat^* -> Denotable-value ->
    Denotable-value -> Denotable-value
update-value = lambda nlist. lambda new-value. lambda current-value.
    null nlist -> new-value
    [] (cases current-value of
        isNatlocn(l) -> inErrvalue()
        ...
        [] isArray(map, l, u) ->
            let n = hd nlist in
            let lnew = (n lt l -> n [] l) in
            let unew = (n gt u -> n [] u)
            in augment-array n (update-value
                (tl nlist) new-value (map n))
                (map, lnew, unew)
        ...
        [] isErrvalue() -> augment-array n
            (update-value (tl nlist) new-value
            inErrvalue()) (empty-array n n)
        ...
    end)