@@ -210,9 +210,9 @@ defined as follows:
210210Inside a ``do`` block, the following syntactic transformations are
211211applied:
212212
213−- ``x <- v; e`` becomes ``v >>= (\backslashx => e)``
213+- ``x <- v; e`` becomes ``v >>= (\x => e)``
214214
215−- ``v; e`` becomes ``v >>= (\backslash_ => e)``
215+- ``v; e`` becomes ``v >>= (\_ => e)``
216216
217217- ``let x = v; e`` becomes ``let x = v in e``
218218
@@ -236,7 +236,7 @@ Using this we can, for example, define a function which adds two
236236 return (x' + y') -- Add them
237237
238238This function will extract the values from ``x`` and ``y``, if they
239−are available, or return ``Nothing`` if they are not. Managing the
239+are both available, or return ``Nothing`` if one or both are not ("fail fast"). Managing the
240240``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the
241241``do`` notation.
242242
@@ -364,7 +364,7 @@ alternative notion of function application, with explicit calls to
364364
365365Rather than having to insert ``m_app`` everywhere there is an
366366application, we can use to do the job for us. To do this, we can make
367−``Maybe`` an instance of ``Applicative`` as follows, where ``<>`` is
367+``Maybe`` an instance of ``Applicative`` as follows, where ``<*>`` is
368368defined in the same way as ``m_app`` above (this is defined in the
369369Idris library):
370370
@@ -376,9 +376,9 @@ Idris library):
376376 (Just f) <*> (Just a) = Just (f a)
377377 _ <*> _ = Nothing
378378
379−Using we can use this instance as follows, where a function
380−application ``[| f a1 …an |]`` is translated into ``pure f <> a1 <>
381−…<> an``:
379+Using ``<*>`` we can use this instance as follows, where a function
380+application ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*>
381+… <*> an``:
382382
383383.. code-block:: idris
384384
@@ -399,7 +399,7 @@ to the following:
399399 | Add Expr Expr -- addition
400400
401401Evaluation will take place relative to a context mapping variables
402−(represented as ``String``\s) to integer values, and can possibly fail.
402+(represented as ``String``\s) to ``Int`` values, and can possibly fail.
403403We define a data type ``Eval`` to wrap an evaluator:
404404
405405.. code-block:: idris