@@ -562,7 +562,7 @@ their types can become quite verbose given that we need to provide explicit
562562input and output resource lists. This is convenient for giving types for
563563the primitive operations, but for more general use it's much more convenient
564564to be able to express *transitions* on individual resources, rather than
565−given input and output resource lists in full. We can do this with
565+giving input and output resource lists in full. We can do this with
566566``ST``:
567567
568568.. code-block:: idris
@@ -574,7 +574,7 @@ given input and output resource lists in full. We can do this with
574574``ST`` is a type level function which computes an appropriate ``STrans``
575575type given a list of *actions*, which describe transitions on resources.
576576An ``Action`` in a function type can take one of the following forms (plus
577−some others which we'll see shortly):
577+some others which we'll see later in the tutorial):
578578
579579* ``lbl ::: ty`` expresses that the resource ``lbl`` begins and ends in
580580 the state ``ty``