we'll just talk about \[[expression]] and let that be a monadic value, implemented in part by a function that takes `(r, h)` as an argument.
- More specifically, \[[expression]] will be a set of `'a dpm`s, where `'a` is the appropriate type for *expression*. Each `'a dpm` is implemented by a function that takes `(r, h)` as an argument.
-
* In def 2.7, GS&V talk about an operation that takes an existing set of discourse possibilities, and *extends* each member in the set by (i) allocating a new location in the store, (ii) putting some entity `d` from the domain in that location, and (iii) assigning variable `x` to that location in the store.
It will be useful to have a shorthand way of referring to this operation:
(* next we assign 'x' to location newindex *)
in let r' = fun v ->
if v = var_to_bind then newindex else r v
- in (r',h')
+ (* the reason for returning true as an initial element will emerge later *)
+ in (true, r',h')
* Is that enough? If not, here are some [more hints](/hints/assignment_7_hint_4).