@@ -334,16 +334,25 @@ importing ``Data.Fin``, or can be declared as follows:
334 FZ : Fin (S k)
334 FZ : Fin (S k)
335 FS : Fin k -> Fin (S k)
335 FS : Fin k -> Fin (S k)
337+From the signature, we can see that this is a data type that takes a ``Nat``, and produces a type.
338+So this is not a set in the sense of a collection that is a container of objects,
339+rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.
340+Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where
341+``n`` is the argument used to instantiate the ``Fin`` type.
342+For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.
344+Let us look at the constructors in greater detail.
337``FZ`` is the zeroth element of a finite set with ``S k`` elements;
346``FZ`` is the zeroth element of a finite set with ``S k`` elements;
338``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
347``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
339elements. ``Fin`` is indexed by a ``Nat``, which represents the number
348elements. ``Fin`` is indexed by a ``Nat``, which represents the number
340of elements in the set. Obviously we can’t construct an element of an
349of elements in the set. Obviously we can’t construct an element of an
341empty set, so neither constructor targets ``Fin Z``.
350empty set, so neither constructor targets ``Fin Z``.
343−A useful application of the ``Fin`` family is to represent bounded
352+As mentioned above, a useful application of the ``Fin`` family is to represent bounded
344natural numbers. Since the first ``n`` natural numbers form a finite
353natural numbers. Since the first ``n`` natural numbers form a finite
345−set of ``n`` elements, we can treat ``Fin n`` as the set of natural
354+set of ``n`` elements, we can treat ``Fin n`` as the set of integers
346−numbers bounded by ``n``.
355+greater than or equal to zero and less than ``n``.
348For example, the following function which looks up an element in a
357For example, the following function which looks up an element in a
349``Vect``, by a bounded index given as a ``Fin n``, is defined in the
358``Vect``, by a bounded index given as a ``Fin n``, is defined in the
@@ -359,7 +368,7 @@ This function looks up a value at a given location in a vector. The
359location is bounded by the length of the vector (``n`` in each case),
368location is bounded by the length of the vector (``n`` in each case),
360so there is no need for a run-time bounds check. The type checker
369so there is no need for a run-time bounds check. The type checker
361guarantees that the location is no larger than the length of the
370guarantees that the location is no larger than the length of the
362−vector.
371+vector, and of course no less than zero.
364Note also that there is no case for ``Nil`` here. This is because it
373Note also that there is no case for ``Nil`` here. This is because it
365is impossible. Since there is no element of ``Fin Z``, and the
374is impossible. Since there is no element of ``Fin Z``, and the