Merge pull request #2151 from jfdm/doc/fixes

Fixes for Idris Tutorial User Docs

docs/tutorial/introduction.rst

@@ -25,11 +25,12 @@ lists of a given length [1]_, ``Vect n a``, where ``a`` is the element
 type and ``n`` is the length of the list and can be an arbitrary term.
 
 When types can contain values, and where those values describe
-properties (e.g. the length of a list) the type of a function can
-begin to describe its own properties. For example, concatenating two
-lists has the property that the resulting list’s length is the sum of
-the lengths of the two input lists. We can therefore give the
-following type to the ``app`` function, which concatenates vectors:
+properties, for example the length of a list, the type of a function
+can begin to describe its own properties. Take for example the
+concatenatation of two lists. This operation has the property that the
+resulting list's length is the sum of the lengths of the two input
+lists. We can therefore give the following type to the ``app``
+function, which concatenates vectors:
 
 .. code-block:: idris
 
@@ -58,11 +59,10 @@ Example Code
 ============
 
 This tutorial includes some example code, which has been tested with
-Idris version . The files are available in the Idris
-distribution, and provided along side the tutorial source, so that you
-can try them out easily, under ``tutorial/examples``. However, it is
-strongly recommended that you can type them in yourself, rather than
-simply loading and reading them.
+against Idris. These files are available with the Idris distribution,
+so that you can try them out easily. They can be found under
+``samples``. It is, however, strongly recommended that you type
+them in yourself, rather than simply loading and reading them.
 
 .. [1]
    Typically, and perhaps confusingly, referred to in the dependently

docs/tutorial/modules.rst

@@ -10,11 +10,11 @@ module, a list of ``import`` statements giving the other modules which
 are to be imported, and a collection of declarations and definitions of
 types, classes and functions. For example, the listing below gives a
 module which defines a binary tree type ``BTree`` (in a file
-``btree.idr``):
+``Btree.idr``):
 
 .. code-block:: idris
 
-    module btree
+    module Btree
 
     data BTree a = Leaf
                  | Node (BTree a) a (BTree a)
@@ -40,23 +40,24 @@ Then, this gives a main program (in a file
 
     module Main
 
-    import btree
+    import Btree
 
     main : IO ()
     main = do let t = toTree [1,8,2,7,9,3]
               print (btree.toList t)
 
 
+
 The same names can be defined in multiple modules. This is possible
 because in practice names are *qualified* with the name of the module.
 The names defined in the ``btree`` module are, in full:
 
-+ ``btree.BTree``
-+ ``btree.Leaf``
-+ ``btree.Node``
-+ ``btree.insert``
-+ ``btree.toList``
-+ ``btree.toTree``
++ ``Btree.BTree``
++ ``Btree.Leaf``
++ ``Btree.Node``
++ ``Btree.insert``
++ ``Btree.toList``
++ ``Btree.toTree``
 
 If names are otherwise unambiguous, there is no need to give the fully
 qualified name. Names can be disambiguated either by giving an explicit
@@ -103,7 +104,7 @@ functions to be exported as ``abstract``, as we see below:
 
 .. code-block:: idris
 
-    module btree
+    module Btree
 
     abstract data BTree a = Leaf
                           | Node (BTree a) a (BTree a)
@@ -137,7 +138,8 @@ the ``public`` modifier on an ``import``. For example:
 
     module A
 
-    import B import public C
+    import B
+    import public C
 
     public a : AType a = ...
 
@@ -154,7 +156,7 @@ wish to overload names within the same module:
 
 .. code-block:: idris
 
-    module foo
+    module Foo
 
     namespace x
       test : Int -> Int

docs/tutorial/starting.rst

@@ -10,12 +10,9 @@ Prerequisites
 Before installing Idris, you will need to make sure you have all
 of the necessary libraries and tools. You will need:
 
-- A fairly recent Haskell platform. Version 2013.2.0.0 should be
-   sufficiently recent, though it is better to be completely up to
-   date.
+- A fairly recent Haskell platform. Version ``2013.2.0.0`` should be sufficiently recent, though it is better to be completely up to date.
 
-- The *GNU Multiple Precision Arithmetic Library* (GMP) is available
-   from MacPorts/Homebrew and all major Linux distributions.
+- The *GNU Multiple Precision Arithmetic Library* (GMP) is available  from MacPorts/Homebrew and all major Linux distributions.
 
 Downloading and Installing
 ==========================
@@ -33,7 +30,7 @@ development version you can find it, as well as build intructions, on
 GitHub at: https://github.com/idris-lang/Idris-dev.
 
 To check that installation has succeeded, and to write your first
-Idris program, create a file called “``hello.idr``” containing the
+Idris program, create a file called ``hello.idr`` containing the
 following text:
 
 .. code-block:: idris
@@ -55,18 +52,17 @@ create an executable called ``hello``, which you can run:
     $ ./hello
     Hello world
 
-Note that the ``$`` indicates the shell prompt! Should the Idris
-executable not be found please ensure that you have added
-``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS X
-users may find they need to use ``~/Library/Haskell/bin``
+Please note that the dollar sign ``$`` indicates the shell prompt!
+Should the Idris executable not be found please ensure that you have
+added ``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS
+X users may find they need to add ``~/Library/Haskell/bin``
 instead. Some useful options to the Idris command are:
 
 - ``-o prog`` to compile to an executable called ``prog``.
 
-- ``--check`` type check the file and its dependencies without
-   starting the interactive environment.
+- ``--check`` type check the file and its dependencies without starting the interactive environment.
 
-- ``--help`` display usage summary and command line options
+- ``--help`` display usage summary and command line options.
 
 The Interactive Environment
 ===========================

docs/tutorial/typesfuns.rst

@@ -12,13 +12,13 @@ Idris defines several primitive types: ``Int``, ``Integer`` and
 manipulation, and ``Ptr`` which represents foreign pointers. There are
 also several data types declared in the library, including ``Bool``,
 with values ``True`` and ``False``. We can declare some constants with
-these types. Enter the following into a file ``prims.idr`` and load it
+these types. Enter the following into a file ``Prims.idr`` and load it
 into the Idris interactive environment by typing ``idris
-prims.idr``:
+Prims.idr``:
 
 .. code-block:: idris
 
-    module prims
+    module Prims
 
     x : Int
     x = 42
@@ -33,17 +33,18 @@ prims.idr``:
     quux = False
 
 An Idris file consists of an optional module declaration (here
-``module prims``) followed by an optional list of imports (none here,
-however Idris programs can consist of several modules, and the
-definitions in each module each have their own namespace, as we will
-discuss in Section :ref:`sect-namespaces`) and a collection of
-declarations and definitions. The order of definitions is significant
-— functions and data types must be defined before use. Each definition
-must have a type declaration, for example see ``x : Int``, ``foo :
-String``, from the above listing. Indentation is significant — a new
-declaration begins at the same level of indentation as the preceding
-declaration.  Alternatively, declarations may be terminated with a
-semicolon.
+``module Prims``) followed by an optional list of imports and a
+collection of declarations and definitions. In this example no imports
+have been specified. However Idris programs can consist of several
+modules and the definitions in each module each have their own
+namespace. This is discussed further in Section
+:ref:`sect-namespaces`). When writing Idris programs both the order in
+definitions are given and indentation are significant. Functions and
+data types must be defined before use, incidently each definition must
+have a type declaration, for example see ``x : Int``, ``foo :
+String``, from the above listing. New declarations must begin at the
+same level of indentation as the preceding declaration.
+Alternatively, a semicolon ``;`` can be used to terminate declarations.
 
 A library module ``prelude`` is automatically imported by every
 Idris program, including facilities for IO, arithmetic, data
@@ -63,7 +64,7 @@ All of the usual arithmetic and comparison operators are defined for
 the primitive types. They are overloaded using type classes, as we
 will discuss in Section :ref:`sect-classes` and can be extended to
 work on user defined types. Boolean expressions can be tested with the
-``if...then...else`` construct:
+``if...then...else`` construct, for example:
 
 ::
 
@@ -73,9 +74,9 @@ work on user defined types. Boolean expressions can be tested with the
 Data Types
 ==========
 
-Data types are declared in a similar way to Haskell data types, with a
-similar syntax. Natural numbers and lists, for example, can be
-declared as follows:
+Data types are declared in a similar way and with similar syntax to
+Haskell. Natural numbers and lists, for example, can be declared as
+follows:
 
 .. code-block:: idris
 
@@ -193,11 +194,13 @@ does not need to be visible globally:
 Indentation is significant — functions in the ``where`` block must be
 indented further than the outer function.
 
-**Scope:** Any names which are visible in the outer scope are also
-visible in the ``where`` clause (unless they have been redefined, such
-as ``xs`` here). A name which appears only in the type will be in scope
-in the ``where`` clause if it is a *parameter* to one of the types,
-i.e. it is fixed across the entire structure.
+.. note:: Scope
+
+    Any names which are visible in the outer scope are also visible in
+    the ``where`` clause (unless they have been redefined, such as ``xs``
+    here). A name which appears only in the type will be in scope in the
+    ``where`` clause if it is a *parameter* to one of the types, i.e. it
+    is fixed across the entire structure.
 
 As well as functions, ``where`` blocks can include local data
 declarations, such as the following where ``MyLT`` is not accessible
@@ -306,16 +309,17 @@ following:
     $ idris vbroken.idr --check
     vbroken.idr:9:23:When elaborating right hand side of Vect.++:
     When elaborating an application of constructor Vect.:::
-            Can't unify
-                    Vect (k + k) a
-            with
-                    Vect (plus k m) a
+        Can't unify
+                Vect (k + k) a (Type of xs ++ xs)
+        with
+                Vect (plus k m) a (Expected type)
+
+        Specifically:
+                Can't unify
+                        plus k k
+                with
+                        plus k m
 
-            Specifically:
-                    Can't unify
-                            plus k k
-                    with
-                            plus k m
 
 This error message suggests that there is a length mismatch between
 two vectors — we needed a vector of length ``k + m``, but provided a

docs/tutorial/views.rst

@@ -83,8 +83,8 @@ rule:
 The value of the result of ``parity k`` affects the form of ``k``,
 because the result of ``parity k`` depends on ``k``. So, as well as
 the patterns for the result of the intermediate computation (``Even``
-and ``odd``) right of the ``\mid``, we also write how the results
-affect the other patterns left of the :math:`\mid`. Note that there is
+and ``odd``) right of the ``|``, we also write how the results
+affect the other patterns left of the ``|``. Note that there is
 a function in the patterns (``+``) and repeated occurrences of
 ``j``—this is allowed because another argument has determined the form
 of these patterns.