@@ -349,7 +349,7 @@ following:
349 $ idris vbroken.idr --check
349 $ idris vbroken.idr --check
350 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
350 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
351 When elaborating an application of constructor Vect.:::
351 When elaborating an application of constructor Vect.:::
352− Type mismatch between
352+ Type mismatch between
353 Vect (k + k) a (Type of xs ++ xs)
353 Vect (k + k) a (Type of xs ++ xs)
355 Vect (plus k m) a (Expected type)
355 Vect (plus k m) a (Expected type)
@@ -442,7 +442,7 @@ names, ``n`` and ``a``, which are not declared explicitly. These are
442Implicit arguments, given in braces ``{}`` in the type declaration,
442Implicit arguments, given in braces ``{}`` in the type declaration,
443are not given in applications of ``index``; their values can be
443are not given in applications of ``index``; their values can be
444inferred from the types of the ``Fin n`` and ``Vect n a``
444inferred 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
446as a parameter or index in a
446as a parameter or index in a
447type declaration, but which is otherwise unbound, will be automatically
447type declaration, but which is otherwise unbound, will be automatically
448bound as an implicit argument. Implicit arguments can still be given
448bound 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:
1022 record Person where
1022 record Person where
1023 constructor MkPerson
1023 constructor MkPerson
1024− name : String
1024+ firstName, middleName, lastName : String
1025 age : Int
1025 age : Int
1027 fred : Person
1027 fred : Person
1028− fred = MkPerson "Fred" 30
1028+ fred = MkPerson "Fred" "Joe" "Bloggs" 30
1030Records can have *parameters*, which are listed between the record
1030Records can have *parameters*, which are listed between the record
1031name and the ``where`` keyword, and *fields*, which are in an indented
1031name and the ``where`` keyword, and *fields*, which are in an indented
1032−block following the `where` keyword (here, ``name`` and ``age``). The
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
1033−constructor name is provided after the ``constructor`` keyword. The
1035+provided after the ``constructor`` keyword. The field names can be used to
1034−field names can be used to access the field values:
1036+access the field values:
1038− *record> name fred
1040+ *record> firstName fred
1039 "Fred" : String
1041 "Fred" : String
1040 *record> age fred
1042 *record> age fred
1041 30 : Int
1043 30 : Int
1042− *record> :t name
1044+ *record> :t firstName
1043− name : Person -> String
1045+ firstName : Person -> String
1045We can also use the field names to update a record (or, more
1047We can also use the field names to update a record (or, more
1046precisely, produce a copy of the record with the given fields
1048precisely, produce a copy of the record with the given fields
@@ -1048,10 +1050,10 @@ updated):
1049.. code-block:: bash
1051.. code-block:: bash
1051− *record> record { name = "Jim" } fred
1053+ *record> record { firstName = "Jim" } fred
1052− MkPerson "Jim" 30 : Person
1054+ MkPerson "Jim" "Joe" "Bloggs" 30 : Person
1053− *record> record { name = "Jim", age = 20 } fred
1055+ *record> record { firstName = "Jim", age = 20 } fred
1054− MkPerson "Jim" 20 : Person
1056+ MkPerson "Jim" "Joe" "Bloggs" 20 : Person
1056The syntax ``record { field = val, ... }`` generates a function which
1058The syntax ``record { field = val, ... }`` generates a function which
1057updates the given fields in a record.
1059updates the given fields in a record.
@@ -1078,7 +1080,7 @@ length because it will not affect the type of the record:
1080 *record> addStudent fred (ClassInfo [] "CS")
1082 *record> addStudent fred (ClassInfo [] "CS")
1081− ClassInfo [MkPerson "Fred" 30] "CS" : Class
1083+ ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
1083Nested record update
1085Nested record update
1084--------------------
1086--------------------