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:
We can call the `(fun (r, g) -> ...)` part \[[Qx]] and then updating `s` with \[[Qx]] will be:
or as it's written using Haskell's infix notation for bind:
or as it's written using Haskell's infix notation for bind:
* 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:
* 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]]