@@ -246,6 +246,70 @@ are both available, or return ``Nothing`` if one or both are not ("fail fast").
246246 *ifaces> m_add (Just 20) Nothing
247247 Nothing : Maybe Int
248248
249+Pattern Matching Bind
250+---------------------
251+
252+Sometimes we want to pattern match immediately on the result of a function
253+in ``do`` notation. For example, let's say we have a function ``readNumber``
254+which reads a number from the console, returning a value of the form
255+``Just x`` if the number is valid, or ``Nothing`` otherwise:
256+
257+.. code-block:: idris
258+
259+ readNumber : IO (Maybe Nat)
260+ readNumber = do
261+ input <- getLine
262+ if all isDigit (unpack input)
263+ then pure (Just (cast input))
264+ else pure Nothing
265+
266+If we then use it to write a function to read two numbers, returning
267+``Nothing`` if neither are valid, then we would like to pattern match
268+on the result of ``readNumber``:
269+
270+.. code-block:: idris
271+
272+ readNumbers : IO (Maybe (Nat, Nat))
273+ readNumbers =
274+ do x <- readNumber
275+ case x of
276+ Nothing => pure Nothing
277+ Just x_ok => do y <- readNumber
278+ case y of
279+ Nothing => pure Nothing
280+ Just y_ok => pure (Just (x_ok, y_ok))
281+
282+If there's a lot of error handling, this could get deeply nested very quickly!
283+So instead, we can combine the bind and the pattern match in one line. For example,
284+we could try pattern matching on values of the form ``Just x_ok``:
285+
286+.. code-block:: idris
287+
288+ readNumbers : IO (Maybe (Nat, Nat))
289+ readNumbers =
290+ do Just x_ok <- readNumber
291+ Just y_ok <- readNumber
292+ pure (Just (x_ok, y_ok))
293+
294+There is still a problem, however, because we've now omitted the case for
295+``Nothing`` so ``readNumbers`` is no longer total! We can add the ``Nothing``
296+case back as follows:
297+
298+.. code-block:: idris
299+
300+ readNumbers : IO (Maybe (Nat, Nat))
301+ readNumbers =
302+ do Just x_ok <- readNumber | Nothing => pure Nothing
303+ Just y_ok <- readNumber | Nothing => pure Nothing
304+ pure (Just (x_ok, y_ok))
305+
306+The effect of this version of ``readNumbers`` is identical to the first (in
307+fact, it is syntactic sugar for it and directly translated back into that form).
308+The first part of each statement (``Just x_ok <-`` and ``Just y_ok <-``) gives
309+the preferred binding - if this matches, execution will continue with the rest
310+of the ``do`` block. The second part gives the alternative bindings, of which
311+there may be more than one.
312+
249313``!``-notation
250314--------------
251315