@@ -346,7 +346,6 @@ can also be accessed with the following syntax:
346346 record { a->b->c } x
347347
348348
349−
350349Dependent Types
351350===============
352351
@@ -493,10 +492,10 @@ elements. ``Fin`` is indexed by a ``Nat``, which represents the number
493492of elements in the set. Since we can’t construct an element of an
494493empty set, neither constructor targets ``Fin Z``.
495494
496−As mentioned above, a useful application of the ``Fin`` family is to represent bounded
497−natural numbers. Since the first ``n`` natural numbers form a finite
498−set of ``n`` elements, we can treat ``Fin n`` as the set of integers
499−greater than or equal to zero and less than ``n``.
495+As mentioned above, a useful application of the ``Fin`` family is to
496+represent bounded natural numbers. Since the first ``n`` natural
497+numbers form a finite set of ``n`` elements, we can treat ``Fin n`` as
498+the set of integers greater than or equal to zero and less than ``n``.
500499
501500For example, the following function which looks up an element in a
502501``Vect``, by a bounded index given as a ``Fin n``, is defined in the
@@ -605,7 +604,7 @@ appear within the block:
605604 There : Elem x xs -> Elem x (y :: xs)
606605
607606Note: Declaration Order and ``mutual`` blocks
608−---------------------------------------------
607+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
609608
610609In general, functions and data types must be defined before use, since
611610dependent types allow functions to appear as part of types, and their
@@ -837,7 +836,7 @@ remember that Idris is still in development, so if you don’t see
837836the function you need, please feel free to add it and submit a patch!
838837
839838Aside: Anonymous functions and operator sections
840−------------------------------------------------
839+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
841840
842841There are actually neater ways to write the above expression. One way
843842would be to use an anonymous function:
@@ -897,8 +896,8 @@ simply ``b``. Since the default value might not be used, we mark it as
897896``Lazy`` in case it is a large expression where evaluating it then
898897discarding it would be wasteful.
899898
900−Tuples and Dependent Pairs
901−--------------------------
899+Tuples
900+------
902901
903902Values can be paired with the following built-in data type:
904903
@@ -994,6 +993,43 @@ intermediate values:
994993
995994We will see more on ``with`` notation later.
996995
996+Dependent Records
997+-----------------
998+
999+Records can also be dependent on values. Records *parameters*, which
1000+are not subject to field updates. The parameters appear as arguments
1001+to the resulting type, and are written following the record type
1002+name. For example, a pair type could be defined as follows:
1003+
1004+.. code-block:: idris
1005+
1006+ record Prod a b where
1007+ constructor Times
1008+ fst : a
1009+ snd : b
1010+
1011+
1012+Using the class record from the original introduction to records. The
1013+size of the class can be restricted using a ``Vect`` and the size
1014+promoted to the type level by parameterising the record with the size.
1015+Foe example:
1016+
1017+
1018+.. code-block:: idris
1019+
1020+ record SizedClass (size : Nat) where
1021+ constructor SizedClassInfo
1022+ students : Vect size Person
1023+ className : String
1024+
1025+**Note** that it is no longer possible to use the ``addStudent``
1026+method from earlier as that would change the size of the class. To provide an add student the function must specify in the type that the size of the class has been increased by one. As the size if specified using natural numbers, the new value can be incremeated using the successor constructor.
1027+
1028+.. code-block:: idris
1029+
1030+ addStudent : Person -> SizedClass n -> SizedClass (S n)
1031+ addStudent p c = record { students = p :: students c } c
1032+
9971033.. _sect-more-expr:
9981034
9991035More Expressions
@@ -1104,40 +1140,3 @@ matching ``let`` and lambda bindings. It will *only* work if:
11041140- The type of the result is "known". i.e. the type of the expression
11051141 can be determined *without* type checking the ``case``-expression
11061142 itself.
1107−
1108−Dependent Records
1109−=================
1110−
1111−Records can also be dependent on values. Records *parameters*, which
1112−are not subject to field updates. The parameters appear as arguments
1113−to the resulting type, and are written following the record type
1114−name. For example, a pair type could be defined as follows:
1115−
1116−.. code-block:: idris
1117−
1118− record Prod a b where
1119− constructor Times
1120− fst : a
1121− snd : b
1122−
1123−
1124−Using the class record from the original introduction to records. The
1125−size of the class can be restricted using a ``Vect`` and the size
1126−promoted to the type level by parameterising the record with the size.
1127−Foe example:
1128−
1129−
1130−.. code-block:: idris
1131−
1132− record SizedClass (size : Nat) where
1133− constructor SizedClassInfo
1134− students : Vect size Person
1135− className : String
1136−
1137−**Note** that it is no longer possible to use the ``addStudent``
1138−method from earlier as that would change the size of the class. To provide an add student the function must specify in the type that the size of the class has been increased by one. As the size if specified using natural numbers, the new value can be incremeated using the successor constructor.
1139−
1140−.. code-block:: idris
1141−
1142− addStudent : Person -> SizedClass n -> SizedClass (S n)
1143− addStudent p c = record { students = p :: students c } c