* They say the denotation of a predicate is whatever extension the world `w` associates with the predicate. Since we don't have worlds, this will just be an extension.
-* They say the denotation of a variable is the object which the store `g` assigns to the index that the assignment function `r` assigns to the variable. In other words, if the variable is `'x'`, its denotation wrt `(r, g, w)` is `g[r['x']]`.
+* They say the denotation of a variable is the object which the store `g` assigns to the index that the assignment function `r` assigns to the variable. In other words, if the variable is `'x'`, its denotation wrt `(r, g, w)` is `g[r['x']]`. In our OCaml implementation, that will be `List.nth g (r 'x')`.
We're going to keep all of that, except dropping the worlds. And instead of talking about