@@ -973,8 +973,8 @@ Dependent Records
974*Records* are data types which collect several values (the record's
974*Records* are data types which collect several values (the record's
975*fields*) together. Idris provides syntax for defining records and
975*fields*) together. Idris provides syntax for defining records and
976−*automatically generating field access and update functions. For
976+*automatically generating field access and update functions*. For
977−*example, we can represent a person's name and age in a record:
977+example, we can represent a person's name and age in a record:
979.. code-block:: idris
979.. code-block:: idris