- 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.
+ we'll just talk about \[[expression]] and let that be a monadic operation, implemented in part by a function that takes `(r, h)` as an argument.
+
+ In particular, the meaning of sentential clauses will be an operation that we monadically bind to an existing `bool dpm set`. Here is its type:
+
+ type clause = bool dpm -> bool dpm set;;