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