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