@@ -349,7 +349,7 @@ following:
349349 $ idris vbroken.idr --check
350350 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
351351 When elaborating an application of constructor Vect.:::
352− Type mismatch between
352+ Type mismatch between
353353 Vect (k + k) a (Type of xs ++ xs)
354354 and
355355 Vect (plus k m) a (Expected type)
@@ -442,7 +442,7 @@ names, ``n`` and ``a``, which are not declared explicitly. These are
442442Implicit arguments, given in braces ``{}`` in the type declaration,
443443are not given in applications of ``index``; their values can be
444444inferred from the types of the ``Fin n`` and ``Vect n a``
445−arguments. Any name beginning with a lower case letter which appears
445+arguments. Any name beginning with a lower case letter which appears
446446as a parameter or index in a
447447type declaration, but which is otherwise unbound, will be automatically
448448bound as an implicit argument. Implicit arguments can still be given
@@ -1021,26 +1021,28 @@ example, we can represent a person's name and age in a record:
10211021
10221022 record Person where
10231023 constructor MkPerson
1024− name : String
1024+ firstName, middleName, lastName : String
10251025 age : Int
10261026
10271027 fred : Person
1028− fred = MkPerson "Fred" 30
1028+ fred = MkPerson "Fred" "Joe" "Bloggs" 30
10291029
10301030Records can have *parameters*, which are listed between the record
10311031name and the ``where`` keyword, and *fields*, which are in an indented
1032−block following the `where` keyword (here, ``name`` and ``age``). The
1033−constructor name is provided after the ``constructor`` keyword. The
1034−field names can be used to access the field values:
1032+block following the `where` keyword (here, ``firstName``, ``middleName``,
1033+``lastName``, and ``age``). You can declare multiple fields on a single
1034+line, provided that they have the same type. The constructor name is
1035+provided after the ``constructor`` keyword. The field names can be used to
1036+access the field values:
10351037
10361038::
10371039
1038− *record> name fred
1040+ *record> firstName fred
10391041 "Fred" : String
10401042 *record> age fred
10411043 30 : Int
1042− *record> :t name
1043− name : Person -> String
1044+ *record> :t firstName
1045+ firstName : Person -> String
10441046
10451047We can also use the field names to update a record (or, more
10461048precisely, produce a copy of the record with the given fields
@@ -1048,10 +1050,10 @@ updated):
10481050
10491051.. code-block:: bash
10501052
1051− *record> record { name = "Jim" } fred
1052− MkPerson "Jim" 30 : Person
1053− *record> record { name = "Jim", age = 20 } fred
1054− MkPerson "Jim" 20 : Person
1053+ *record> record { firstName = "Jim" } fred
1054+ MkPerson "Jim" "Joe" "Bloggs" 30 : Person
1055+ *record> record { firstName = "Jim", age = 20 } fred
1056+ MkPerson "Jim" "Joe" "Bloggs" 20 : Person
10551057
10561058The syntax ``record { field = val, ... }`` generates a function which
10571059updates the given fields in a record.
@@ -1078,7 +1080,7 @@ length because it will not affect the type of the record:
10781080::
10791081
10801082 *record> addStudent fred (ClassInfo [] "CS")
1081− ClassInfo [MkPerson "Fred" 30] "CS" : Class
1083+ ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
10821084
10831085Nested record update
10841086--------------------