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

Array Assignment

C[[I[S] := E]] = lambda e.lambda s.
    cases (accessenv [[I]] e) of
    ...
    [] isArray(a) ->
        (cases (S[[S]]a e s) of
        ...
        isNatlocn(l) ->
            (cases (E[[E]]e s) of
            ...
            [] isNat(n) ->
                return(update l inNat(n) s)
            ...
            end)
        ...
        end)
    ...
    end

Assignment is first order (location, not an array, is on left-hand-side).