@@ -562,7 +562,7 @@ their types can become quite verbose given that we need to provide explicit
562input and output resource lists. This is convenient for giving types for
562input and output resource lists. This is convenient for giving types for
563the primitive operations, but for more general use it's much more convenient
563the primitive operations, but for more general use it's much more convenient
564to be able to express *transitions* on individual resources, rather than
564to 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
568.. code-block:: idris
568.. code-block:: idris
@@ -574,7 +574,7 @@ given input and output resource lists in full. We can do this with
574``ST`` is a type level function which computes an appropriate ``STrans``
574``ST`` is a type level function which computes an appropriate ``STrans``
575type given a list of *actions*, which describe transitions on resources.
575type given a list of *actions*, which describe transitions on resources.
576An ``Action`` in a function type can take one of the following forms (plus
576An ``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):
579* ``lbl ::: ty`` expresses that the resource ``lbl`` begins and ends in
579* ``lbl ::: ty`` expresses that the resource ``lbl`` begins and ends in
580 the state ``ty``
580 the state ``ty``