Merge pull request #146 from edwinb/docupdates

Small documentation updates

docs/source/tutorial/starting.rst

@@ -28,14 +28,14 @@ You can download the Idris 2 source from the `Idris web site
 <https://www.idris-lang.org/pages/download.html>`_ or get the latest
 development version from `idris-lang/Idris2
 <https://github.com/idris-lang/Idris2>`_ on Github.  This includes the Idris 2
-source code and the Scheme code code generated from that.  Once you have
+source code and the Scheme code generated from that.  Once you have
 unpacked the source, you can install it as follows::
 
     make bootstrap SCHEME=chez
 
 Where `chez` is the executable name of the Chez Scheme compiler. This will
-vary from system to system, but is often one of `scheme`, `chezscheme`, or
-`chezscheme9.5`. If you are building via Racket, you can install it as
+vary from system to system, but is often one of ``scheme``, ``chezscheme``, or
+``chezscheme9.5``. If you are building via Racket, you can install it as
 follows::
 
     make bootstrap-racket

docs/source/tutorial/typesfuns.rst

@@ -234,6 +234,37 @@ of how this works in practice:
 
 .. _sect-holes:
 
+Totality and Covering
+---------------------
+
+By default, functions in Idris must be ``covering``. That is, there must be
+patterns which cover all possible values of the inputs types. For example,
+the following definition will give an error:
+
+.. code-block:: idris
+
+    fromMaybe : Maybe a -> a
+    fromMaybe (Just x) = x
+
+This gives an error because ``fromMaybe Nothing`` is not defined. Idris
+reports:
+
+::
+
+    frommaybe.idr:1:1--2:1:fromMaybe is not covering. Missing cases:
+            fromMaybe Nothing
+
+You can override this with a ``partial`` annotation:
+
+.. code-block:: idris
+
+    partial fromMaybe : Maybe a -> a
+    fromMaybe (Just x) = x
+
+However, this is not advisable, and in general you should only do this during
+the initial development of a function, or during debugging.  If you try to
+evaluate ``fromMaybe Nothing`` at run time you will get a run time error.
+
 Holes
 -----
 

docs/source/updates/updates.rst

@@ -425,6 +425,21 @@ can see if we try evaluating ``myShow True`` at the REPL:
 In fact, this is how interfaces are elaborated. However, ``%hint`` should be
 used with care. Too many hints can lead to a large search space!
 
+Record fields
+-------------
+
+Record fields can now be accessed via a ``.``. For example, if you have:
+
+.. code-block:: idris
+
+    record Person where
+        constructor MkPerson
+        firstName, middleName, lastName : String
+        age : Int
+
+and you have a record ``fred : Person``, then you can use ``fred.firstName``
+to access the ``firstName`` field.
+
 Totality and Coverage
 ---------------------