@@ -248,104 +248,6 @@ So, for example, the following definitions are legal:
248248 where z w = y + w
249249
250250
251−Records
252−=======
253−
254−*Records* are data types which collect several values (the record's
255−*fields*) together. Idris provides syntax for defining records and
256−*automatically generating field access and update functions*. Unlike
257−*the syntax used for data structures, records in Idris follow a
258−*different syntax to that seen with Haskell. For example, we can
259−*represent a person's name and age in a record:
260−
261−.. code-block:: idris
262−
263− record Person where
264− constructor MkPerson
265− firstName, middleName, lastName : String
266− age : Int
267−
268− fred : Person
269− fred = MkPerson "Fred" "Joe" "Bloggs" 30
270−
271−
272−The constructor name is provided using the ``constructor`` keyword,
273−and the *fields* are then given which are in an indented block
274−following the `where` keyword (here, ``firstName``, ``middleName``,
275−``lastName``, and ``age``). You can declare multiple fields on a
276−single line, provided that they have the same type. The field names
277−can be used to access the field values:
278−
279−::
280−
281− *record> firstName fred
282− "Fred" : String
283− *record> age fred
284− 30 : Int
285− *record> :t firstName
286− firstName : Person -> String
287−
288−We can also use the field names to update a record (or, more
289−precisely, produce a copy of the record with the given fields
290−updated):
291−
292−.. code-block:: bash
293−
294− *record> record { firstName = "Jim" } fred
295− MkPerson "Jim" "Joe" "Bloggs" 30 : Person
296− *record> record { firstName = "Jim", age = 20 } fred
297− MkPerson "Jim" "Joe" "Bloggs" 20 : Person
298−
299−The syntax ``record { field = val, ... }`` generates a function which
300−updates the given fields in a record.
301−
302−Records, and fields within records, can have dependent types. Updates
303−are allowed to change the type of a field, provided that the result is
304−well-typed.
305−
306−.. code-block:: idris
307−
308− record Class where
309− constructor ClassInfo
310− students : Vect n Person
311− className : String
312−
313−It is safe to update the ``students`` field to a vector of a different
314−length because it will not affect the type of the record:
315−
316−.. code-block:: idris
317−
318− addStudent : Person -> Class -> Class
319− addStudent p c = record { students = p :: students c } c
320−
321−::
322−
323− *record> addStudent fred (ClassInfo [] "CS")
324− ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
325−
326−
327−Nested record update
328−--------------------
329−
330−Idris also provides a convenient syntax for accessing and updating
331−nested records. For example, if a field is accessible with the
332−expression ``c (b (a x))``, it can be updated using the following
333−syntax:
334−
335−.. code-block:: idris
336−
337− record { a->b->c = val } x
338−
339−This returns a new record, with the field accessed by the path
340−``a->b->c`` set to ``x``. The syntax is first class, i.e. ``record {
341−a->b->c = val }`` itself has a function type. Symmetrically, the field
342−can also be accessed with the following syntax:
343−
344−.. code-block:: idris
345−
346− record { a->b->c } x
347−
348−
349251Dependent Types
350252===============
351253
@@ -993,6 +895,105 @@ intermediate values:
993895
994896We will see more on ``with`` notation later.
995897
898+
899+Records
900+-------
901+
902+*Records* are data types which collect several values (the record's
903+*fields*) together. Idris provides syntax for defining records and
904+*automatically generating field access and update functions*. Unlike
905+*the syntax used for data structures, records in Idris follow a
906+*different syntax to that seen with Haskell. For example, we can
907+*represent a person's name and age in a record:
908+
909+.. code-block:: idris
910+
911+ record Person where
912+ constructor MkPerson
913+ firstName, middleName, lastName : String
914+ age : Int
915+
916+ fred : Person
917+ fred = MkPerson "Fred" "Joe" "Bloggs" 30
918+
919+
920+The constructor name is provided using the ``constructor`` keyword,
921+and the *fields* are then given which are in an indented block
922+following the `where` keyword (here, ``firstName``, ``middleName``,
923+``lastName``, and ``age``). You can declare multiple fields on a
924+single line, provided that they have the same type. The field names
925+can be used to access the field values:
926+
927+::
928+
929+ *record> firstName fred
930+ "Fred" : String
931+ *record> age fred
932+ 30 : Int
933+ *record> :t firstName
934+ firstName : Person -> String
935+
936+We can also use the field names to update a record (or, more
937+precisely, produce a copy of the record with the given fields
938+updated):
939+
940+.. code-block:: bash
941+
942+ *record> record { firstName = "Jim" } fred
943+ MkPerson "Jim" "Joe" "Bloggs" 30 : Person
944+ *record> record { firstName = "Jim", age = 20 } fred
945+ MkPerson "Jim" "Joe" "Bloggs" 20 : Person
946+
947+The syntax ``record { field = val, ... }`` generates a function which
948+updates the given fields in a record.
949+
950+Records, and fields within records, can have dependent types. Updates
951+are allowed to change the type of a field, provided that the result is
952+well-typed.
953+
954+.. code-block:: idris
955+
956+ record Class where
957+ constructor ClassInfo
958+ students : Vect n Person
959+ className : String
960+
961+It is safe to update the ``students`` field to a vector of a different
962+length because it will not affect the type of the record:
963+
964+.. code-block:: idris
965+
966+ addStudent : Person -> Class -> Class
967+ addStudent p c = record { students = p :: students c } c
968+
969+::
970+
971+ *record> addStudent fred (ClassInfo [] "CS")
972+ ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
973+
974+
975+Nested record update
976+~~~~~~~~~~~~~~~~~~~~
977+
978+Idris also provides a convenient syntax for accessing and updating
979+nested records. For example, if a field is accessible with the
980+expression ``c (b (a x))``, it can be updated using the following
981+syntax:
982+
983+.. code-block:: idris
984+
985+ record { a->b->c = val } x
986+
987+This returns a new record, with the field accessed by the path
988+``a->b->c`` set to ``x``. The syntax is first class, i.e. ``record {
989+a->b->c = val }`` itself has a function type. Symmetrically, the field
990+can also be accessed with the following syntax:
991+
992+.. code-block:: idris
993+
994+ record { a->b->c } x
995+
996+
996997Dependent Records
997998-----------------
998999