@@ -232,7 +232,7 @@ Using this we can, for example, define a function which adds two
232232 m_add : Maybe Int -> Maybe Int -> Maybe Int
233233 m_add x y = do x' <- x -- Extract value from x
234234 y' <- y -- Extract value from y
235− return (x' + y') -- Add them
235+ pure (x' + y') -- Add them
236236
237237This function will extract the values from ``x`` and ``y``, if they
238238are both available, or return ``Nothing`` if one or both are not ("fail fast"). Managing the
@@ -270,7 +270,7 @@ on the result of ``readNumber``:
270270.. code-block:: idris
271271
272272 readNumbers : IO (Maybe (Nat, Nat))
273− readNumbers =
273+ readNumbers =
274274 do x <- readNumber
275275 case x of
276276 Nothing => pure Nothing
@@ -286,7 +286,7 @@ we could try pattern matching on values of the form ``Just x_ok``:
286286.. code-block:: idris
287287
288288 readNumbers : IO (Maybe (Nat, Nat))
289− readNumbers =
289+ readNumbers =
290290 do Just x_ok <- readNumber
291291 Just y_ok <- readNumber
292292 pure (Just (x_ok, y_ok))
@@ -298,7 +298,7 @@ case back as follows:
298298.. code-block:: idris
299299
300300 readNumbers : IO (Maybe (Nat, Nat))
301− readNumbers =
301+ readNumbers =
302302 do Just x_ok <- readNumber | Nothing => pure Nothing
303303 Just y_ok <- readNumber | Nothing => pure Nothing
304304 pure (Just (x_ok, y_ok))
@@ -321,7 +321,7 @@ shorthand version, as follows:
321321.. code-block:: idris
322322
323323 m_add : Maybe Int -> Maybe Int -> Maybe Int
324− m_add x y = return (!x + !y)
324+ m_add x y = pure (!x + !y)
325325
326326The notation ``!expr`` means that the expression ``expr`` should be
327327evaluated and then implicitly bound. Conceptually, we can think of