Signed-off-by: Jim Pryor <profjim@jimpryor.net>
We can call the `(fun (r, g) -> ...)` part \[[Qx]] and then updating `s` with \[[Qx]] will be:
- bind_set s [[Qx]]
+ bind_set s \[[Qx]]
or as it's written using Haskell's infix notation for bind:
- s >>= [[Qx]]
+ s >>= \[[Qx]]
* Now how shall we handle \[[∃x]]. As we said, GS&V really tell us how to interpret \[[∃xPx]], but what they say about this breaks naturally into two pieces, such that we can represent the update of `s` with \[[∃xPx]] as:
- s >>= [[∃x]] >>= [[Px]]
+ s >>= \[[∃x]] >>= \[[Px]]