@@ -469,7 +469,7 @@ It is a matter of taste whether you want to do this — sometimes it can
469help document a function by making the purpose of an argument more
469help document a function by making the purpose of an argument more
472−Furthermore, ``{}`` can be used to pattern match on the left hand side, i.e.
472+Furthermore, ``{}`` can be used to pattern match on the left hand side, i.e.
473``{var = pat}`` gets an implicit variable and attempts to pattern match on "pat";
473``{var = pat}`` gets an implicit variable and attempts to pattern match on "pat";
474For example :
474For example :
@@ -1074,7 +1074,7 @@ The syntax ``record { field = val, ... }`` generates a function which
1074updates the given fields in a record. ``=`` assigns a new value to a field,
1074updates the given fields in a record. ``=`` assigns a new value to a field,
1075and ``$=`` applies a function to update its value.
1075and ``$=`` applies a function to update its value.
1077−Each record is defined in its own namespace, which means that field names
1077+Each record is defined in its own namespace, which means that field names
1078can be reused in multiple records.
1078can be reused in multiple records.
1080Records, and fields within records, can have dependent types. Updates
1080Records, and fields within records, can have dependent types. Updates
@@ -1331,6 +1331,7 @@ at runtime if called on an empty list. (This is similar to the behavior of
1331Haskell's ``head`` function.) ``unsafeHead`` might look like this:
1331Haskell's ``head`` function.) ``unsafeHead`` might look like this:
1333.. code-block:: idris
1333.. code-block:: idris
1334 -- Unsafe head example!
1335 -- Unsafe head example!
1335 unsafeHead : List a -> a
1336 unsafeHead : List a -> a
1336 unsafeHead (x::xs) = x
1337 unsafeHead (x::xs) = x