-Compare the new definitions of `safe_add3` and `safe_div3` closely: the definition
-for `safe_add3` shows what it looks like to equip an ordinary operation to
-survive in dangerous presupposition-filled world. Note that the new
-definition of `safe_add3` does not need to test whether its arguments are
-`None` values or real numbers---those details are hidden inside of the
-`bind` function.
-
-Note also that our definition of `safe_div3` recovers some of the simplicity of
-the original `safe_div`, without the complexity introduced by `safe_div2`. We now
-add exactly what extra is needed to track the no-division-by-zero presupposition. Here, too, we don't
-need to keep track of what other presuppositions may have already failed
-for whatever reason on our inputs.
-
-(Linguistics note: Dividing by zero is supposed to feel like a kind of
-presupposition failure. If we wanted to adapt this approach to
-building a simple account of presupposition projection, we would have
-to do several things. First, we would have to make use of the
-polymorphism of the `option` type. In the arithmetic example, we only
-made use of `int option`s, but when we're composing natural language
-expression meanings, we'll need to use types like `N option`, `Det option`,
-`VP option`, and so on. But that works automatically, because we can use
-any type for the `'a` in `'a option`. Ultimately, we'd want to have a
-theory of accommodation, and a theory of the situations in which
-material within the sentence can satisfy presuppositions for other
-material that otherwise would trigger a presupposition violation; but,
-not surprisingly, these refinements will require some more
-sophisticated techniques than the super-simple Option/Maybe monad.)