references

ref e ↦* ref v ↦ l l location ———–> v !e ↦ !l ↦ v e := e' ↦* l := v ↦()

to implement iarray int ref A

ref(int -> int) index: any int initialized 0 l ↦ v:A

new:unit->iarray

new ()↦*iarray access: iarray-> int-> int index element

a[i]

update: iarray->int-> int->unit index value

new: λ_:unit. ref(λi:int.0) iarray:ref(int->int)

access: λa:iarray. λi:int. !a i int->int

update

correct answer

update: λa:iarray.λi:int.λn:int

let x=e in e' = (λx:A.e') e