@@ -12,13 +12,13 @@ Idris defines several primitive types: ``Int``, ``Integer`` and
1212manipulation, and ``Ptr`` which represents foreign pointers. There are
1313also several data types declared in the library, including ``Bool``,
1414with values ``True`` and ``False``. We can declare some constants with
15−these types. Enter the following into a file ``prims.idr`` and load it
15+these types. Enter the following into a file ``Prims.idr`` and load it
1616into the Idris interactive environment by typing ``idris
17−prims.idr``:
17+Prims.idr``:
1818
1919.. code-block:: idris
2020
21− module prims
21+ module Prims
2222
2323 x : Int
2424 x = 42
@@ -33,17 +33,18 @@ prims.idr``:
3333 quux = False
3434
3535An Idris file consists of an optional module declaration (here
36−``module prims``) followed by an optional list of imports (none here,
37−however Idris programs can consist of several modules, and the
38−definitions in each module each have their own namespace, as we will
39−discuss in Section :ref:`sect-namespaces`) and a collection of
40−declarations and definitions. The order of definitions is significant
41−— functions and data types must be defined before use. Each definition
42−must have a type declaration, for example see ``x : Int``, ``foo :
43−String``, from the above listing. Indentation is significant — a new
44−declaration begins at the same level of indentation as the preceding
45−declaration. Alternatively, declarations may be terminated with a
46−semicolon.
36+``module Prims``) followed by an optional list of imports and a
37+collection of declarations and definitions. In this example no imports
38+have been specified. However Idris programs can consist of several
39+modules and the definitions in each module each have their own
40+namespace. This is discussed further in Section
41+:ref:`sect-namespaces`). When writing Idris programs both the order in
42+definitions are given and indentation are significant. Functions and
43+data types must be defined before use, incidently each definition must
44+have a type declaration, for example see ``x : Int``, ``foo :
45+String``, from the above listing. New declarations must begin at the
46+same level of indentation as the preceding declaration.
47+Alternatively, a semicolon ``;`` can be used to terminate declarations.
4748
4849A library module ``prelude`` is automatically imported by every
4950Idris program, including facilities for IO, arithmetic, data
@@ -63,7 +64,7 @@ All of the usual arithmetic and comparison operators are defined for
6364the primitive types. They are overloaded using type classes, as we
6465will discuss in Section :ref:`sect-classes` and can be extended to
6566work on user defined types. Boolean expressions can be tested with the
66−``if...then...else`` construct:
67+``if...then...else`` construct, for example:
6768
6869::
6970
@@ -73,9 +74,9 @@ work on user defined types. Boolean expressions can be tested with the
7374Data Types
7475==========
7576
76−Data types are declared in a similar way to Haskell data types, with a
77−similar syntax. Natural numbers and lists, for example, can be
78−declared as follows:
77+Data types are declared in a similar way and with similar syntax to
78+Haskell. Natural numbers and lists, for example, can be declared as
79+follows:
7980
8081.. code-block:: idris
8182
@@ -193,11 +194,13 @@ does not need to be visible globally:
193194Indentation is significant — functions in the ``where`` block must be
194195indented further than the outer function.
195196
196−**Scope:** Any names which are visible in the outer scope are also
197−visible in the ``where`` clause (unless they have been redefined, such
198−as ``xs`` here). A name which appears only in the type will be in scope
199−in the ``where`` clause if it is a *parameter* to one of the types,
200−i.e. it is fixed across the entire structure.
197+.. note:: Scope
198+
199+ Any names which are visible in the outer scope are also visible in
200+ the ``where`` clause (unless they have been redefined, such as ``xs``
201+ here). A name which appears only in the type will be in scope in the
202+ ``where`` clause if it is a *parameter* to one of the types, i.e. it
203+ is fixed across the entire structure.
201204
202205As well as functions, ``where`` blocks can include local data
203206declarations, such as the following where ``MyLT`` is not accessible
@@ -306,16 +309,17 @@ following:
306309 $ idris vbroken.idr --check
307310 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
308311 When elaborating an application of constructor Vect.:::
309− Can't unify
310− Vect (k + k) a
311− with
312− Vect (plus k m) a
313−
314− Specifically:
315− Can't unify
316− plus k k
317− with
318− plus k m
312+ Can't unify
313+ Vect (k + k) a (Type of xs ++ xs)
314+ with
315+ Vect (plus k m) a (Expected type)
316+
317+ Specifically:
318+ Can't unify
319+ plus k k
320+ with
321+ plus k m
322+
319323
320324This error message suggests that there is a length mismatch between
321325two vectors — we needed a vector of length ``k + m``, but provided a