Signed-off-by: Jim Pryor <profjim@jimpryor.net>
* 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]]
+<pre><code>
+s >>= \[[∃x]] >>= \[[Px]]
+</code></pre>