@@ -25,11 +25,12 @@ lists of a given length [1]_, ``Vect n a``, where ``a`` is the element
25type and ``n`` is the length of the list and can be an arbitrary term.
25type and ``n`` is the length of the list and can be an arbitrary term.
27When types can contain values, and where those values describe
27When types can contain values, and where those values describe
28−properties (e.g. the length of a list) the type of a function can
28+properties, for example the length of a list, the type of a function
29−begin to describe its own properties. For example, concatenating two
29+can begin to describe its own properties. Take for example the
30+concatenatation of two lists. This operation has the property that the
30−lists has the property that the resulting list’s length is the sum of
31+resulting list's length is the sum of the lengths of the two input
31−the lengths of the two input lists. We can therefore give the
32+lists. We can therefore give the following type to the ``app``
32−following type to the ``app`` function, which concatenates vectors:
33+function, which concatenates vectors:
34.. code-block:: idris
35.. code-block:: idris
@@ -58,11 +59,10 @@ Example Code
58============
59============
60This tutorial includes some example code, which has been tested with
61This tutorial includes some example code, which has been tested with
61−Idris version . The files are available in the Idris
62+against Idris. These files are available with the Idris distribution,
62−distribution, and provided along side the tutorial source, so that you
63−can try them out easily, under ``tutorial/examples``. However, it is
63+so that you can try them out easily. They can be found under
64−strongly recommended that you can type them in yourself, rather than
64+``samples``. It is, however, strongly recommended that you type
65−simply loading and reading them.
65+them in yourself, rather than simply loading and reading them.
68 Typically, and perhaps confusingly, referred to in the dependently
68 Typically, and perhaps confusingly, referred to in the dependently