@@ -210,9 +210,9 @@ defined as follows:
210Inside a ``do`` block, the following syntactic transformations are
210Inside a ``do`` block, the following syntactic transformations are
213−- ``x <- v; e`` becomes ``v >>= (\backslashx => e)``
213+- ``x <- v; e`` becomes ``v >>= (\x => e)``
215−- ``v; e`` becomes ``v >>= (\backslash_ => e)``
215+- ``v; e`` becomes ``v >>= (\_ => e)``
217- ``let x = v; e`` becomes ``let x = v in e``
217- ``let x = v; e`` becomes ``let x = v in e``
@@ -236,7 +236,7 @@ Using this we can, for example, define a function which adds two
236 return (x' + y') -- Add them
236 return (x' + y') -- Add them
238This function will extract the values from ``x`` and ``y``, if they
238This 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
240``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the
240``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the
241``do`` notation.
241``do`` notation.
@@ -364,7 +364,7 @@ alternative notion of function application, with explicit calls to
365Rather than having to insert ``m_app`` everywhere there is an
365Rather than having to insert ``m_app`` everywhere there is an
366application, we can use to do the job for us. To do this, we can make
366application, 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
368defined in the same way as ``m_app`` above (this is defined in the
368defined in the same way as ``m_app`` above (this is defined in the
369Idris library):
369Idris library):
@@ -376,9 +376,9 @@ Idris library):
376 (Just f) <*> (Just a) = Just (f a)
376 (Just f) <*> (Just a) = Just (f a)
377 _ <*> _ = Nothing
377 _ <*> _ = Nothing
379−Using we can use this instance as follows, where a function
379+Using ``<*>`` we can use this instance as follows, where a function
380−application ``[| f a1 …an |]`` is translated into ``pure f <> a1 <>
380+application ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*>
381−…<> an``:
381+… <*> an``:
383.. code-block:: idris
383.. code-block:: idris
@@ -399,7 +399,7 @@ to the following:
399 | Add Expr Expr -- addition
399 | Add Expr Expr -- addition
401Evaluation will take place relative to a context mapping variables
401Evaluation 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.
403We define a data type ``Eval`` to wrap an evaluator:
403We define a data type ``Eval`` to wrap an evaluator:
405.. code-block:: idris
405.. code-block:: idris