@@ -352,7 +352,7 @@ than directly with ``delete``.
353We can complete ``getData`` as follows, using a pattern matching bind
353We can complete ``getData`` as follows, using a pattern matching bind
354alternative (see the Idris tutorial, :ref:`monadsdo`) rather than a
354alternative (see the Idris tutorial, :ref:`monadsdo`) rather than a
355−``case`` statement to catch the possibilty of an error with ``login``:
355+``case`` statement to catch the possibility of an error with ``login``:
357.. code-block:: idris
357.. code-block:: idris
@@ -367,7 +367,7 @@ alternative (see the Idris tutorial, :ref:`monadsdo`) rather than a
367 disconnect st
367 disconnect st
369We can't yet try this out, however, because we don't have any implementations
369We can't yet try this out, however, because we don't have any implementations
370−of ``getData``! If we try to execute it in an ``IO`` context, for example,
370+of ``DataStore``! If we try to execute it in an ``IO`` context, for example,
371we'll get an error saying that there's no implementation of ``DataStore IO``:
371we'll get an error saying that there's no implementation of ``DataStore IO``:
@@ -383,7 +383,7 @@ of ``DataStore``.
383Implementing the interface
383Implementing the interface
384==========================
384==========================
386−To execute ``getData`` in ``IO``, we'll need to provided an implementation
386+To execute ``getData`` in ``IO``, we'll need to provide an implementation
387of ``DataStore`` which works in the ``IO`` context. We can begin as
387of ``DataStore`` which works in the ``IO`` context. We can begin as
@@ -526,7 +526,7 @@ like ``getData``, and constrain by only the interfaces we need, rather than
526using a concrete context ``IO``.
526using a concrete context ``IO``.
528We've now seen how to manipulate states, and how to encapsulate state
528We've now seen how to manipulate states, and how to encapsulate state
529−transitions for a specific system like the data store inn an interface.
529+transitions for a specific system like the data store in an interface.
530However, realistic systems will need to *compose* state machines. We'll
530However, realistic systems will need to *compose* state machines. We'll
531either need to use more than one state machine at a time, or implement one
531either need to use more than one state machine at a time, or implement one
532state machine in terms of one or more others. We'll see how to achieve this
532state machine in terms of one or more others. We'll see how to achieve this