Merge pull request #2047 from jfdm/userdocs/package-creation

Add section on package creation, and typo fixes.

docs/effects/conclusions.rst

@@ -5,7 +5,7 @@ Further Reading
 ===============
 
 This tutorial has given an introduction to writing and reasoning about
-side-effecting programs in ``Idris``, using the ``Effects`` library.
+side-effecting programs in Idris, using the ``Effects`` library.
 More details about the *implementation* of the library, such as how
 ``run`` works, how handlers are invoked, etc, are given in a separate
 paper [1]_.

docs/effects/hangman.rst

@@ -264,7 +264,7 @@ generator, then pick a random ``Fin`` to index into a list of
 .. note::
     Rather than have to explicitly declare a type with the vector’s
     length, it is convenient to give a metavariable ``?wtype`` and let
-    ``Idris``’s proof search mechanism find the type. This is a
+    Idris’s proof search mechanism find the type. This is a
     limited form of type inference, but very useful in practice.
 
 

docs/effects/introduction.rst

@@ -14,10 +14,10 @@ and supports programming and reasoning with side-effecting programs,
 supporting mutable state, interaction with the outside world,
 exceptions, and verified resource management.
 
-This tutorial assumes familiarity with pure programming in ``Idris``,
+This tutorial assumes familiarity with pure programming in Idris,
 as described in Sections 1–6 of the main tutorial [1]_. The examples
-are presented are tested with ``Idris`` and can be found in the
-examples directory of the ``Idris`` repository.
+are presented are tested with Idris and can be found in the
+examples directory of the Idris repository.
 
 Consider, for example, the following introductory function which
 illustrates the kind of properties which can be expressed in the type
@@ -47,7 +47,7 @@ able to apply the ``vadd`` function? Before doing so, we will have to:
 
 The complete program will include side-effects for I/O and error
 handling, before we can get to the pure core functionality. In this
-tutorial, we will see how ``Idris`` supports side-effects.
+tutorial, we will see how Idris supports side-effects.
 Furthermore, we will see how we can use the dependent type system to
 *reason* about stateful and side-effecting programs. We will return to
 this specific example later.
@@ -78,7 +78,7 @@ returns the unit value.  All programs using the ``Effects`` library must
 ``import Effects``.  The details of the ``Eff`` type will be presented in the
 remainder of this tutorial.
 
-To compile and run this program, ``Idris`` needs to be told to include
+To compile and run this program, Idris needs to be told to include
 the ``Effects`` package, using the ``-p effects`` flag (this flag is
 required for all examples in this tutorial):
 

docs/effects/simpleeff.rst

@@ -592,7 +592,7 @@ which ``eval`` can be ``run`` to those which support ``STDIO``, such
 as ``IO``. Once effect lists get longer, it can be a good idea instead
 to encapsulate sets of effects in a type synonym. This is achieved as
 follows, simply by defining a function which computes a type, since
-types are first class in ``Idris``:
+types are first class in Idris:
 
 .. code-block:: idris
 

docs/effects/state.rst

@@ -77,7 +77,7 @@ explicit.
 Introducing ``Effects``
 -----------------------
 
-``Idris`` provides a library, ``Effects`` [3]_, which captures this
+Idris provides a library, ``Effects`` [3]_, which captures this
 pattern and many others involving effectful computation [1]_. An
 effectful program ``f`` has a type of the following form:
 

docs/index.rst

@@ -35,6 +35,7 @@ The Idris Tutorial
    tutorial/typesfuns
    tutorial/classes
    tutorial/modules
+   tutorial/packages
    tutorial/interp
    tutorial/views
    tutorial/theorems

docs/reference/erasure.rst

@@ -94,11 +94,11 @@ cannot get below O(n) with time complexities.
 One could argue that Idris in fact compiles ``Nat`` via GMP but
 that's a moot point for two reasons:
 
-* First, whenever we try to index our datastructures with anything
-else than ``Nat``, the compiler is not going to come to the rescue.
++ First, whenever we try to index our datastructures with anything
+  else than ``Nat``, the compiler is not going to come to the rescue.
 
-* Second, even with ``Nat``, the GMP integers are *still* there and
-they slow the runtime down.
++ Second, even with ``Nat``, the GMP integers are *still* there and
+  they slow the runtime down.
 
 This ought not to be the case since the ``Nat`` are never used at
 runtime and they are only there for typechecking purposes. Hence we

docs/tutorial/classes.rst

@@ -366,7 +366,7 @@ Rather than having to insert ``m_app`` everywhere there is an
 application, we can use to do the job for us. To do this, we can make
 ``Maybe`` an instance of ``Applicative`` as follows, where ``<>`` is
 defined in the same way as ``m_app`` above (this is defined in the
-``Idris`` library):
+Idris library):
 
 .. code-block:: idris
 
@@ -481,7 +481,7 @@ Given the following list:
     testList = [3,4,1]
 
 We can sort it using the default ``Ord`` instance, then the named
-instance ``myord`` as follows, at the ``Idris`` prompt:
+instance ``myord`` as follows, at the Idris prompt:
 
 ::
 

docs/tutorial/conclusions.rst

@@ -4,10 +4,10 @@
 Further Reading
 ===============
 
-Further information about ``Idris`` programming, and programming with
+Further information about Idris programming, and programming with
 dependent types in general, can be obtained from various sources:
 
--  The ``Idris`` web site (http://idris-lang.org/) and by asking
+-  The Idris web site (http://idris-lang.org/) and by asking
    questions on the mailing list.
 
 -  The IRC channel ``#idris``, on
@@ -21,14 +21,14 @@ dependent types in general, can be obtained from various sources:
    -  https://github.com/idris-lang/Idris-dev/wiki/Language-Features
 
 - Examining the prelude and exploring the ``samples`` in the
-   distribution. The ``Idris`` source can be found online at:
+   distribution. The Idris source can be found online at:
    https://github.com/idris-lang/Idris-dev.
 
 -  Existing projects on the ``Idris Hackers`` web space:
    http://idris-hackers.github.io.
 
 - Various papers (e.g. [1]_, [2]_, and [3]_).  Although these mostly
-   describe older versions of ``Idris``.
+   describe older versions of Idris.
 
 .. [1] Edwin Brady and Kevin Hammond. 2012. Resource-Safe systems
        programming with embedded domain specific languages. In

docs/tutorial/index.rst

@@ -23,6 +23,7 @@ The is the Idris Tutorial. It will teach you about programming in the Idris Lang
    typesfuns
    classes
    modules
+   packages
    interp
    views
    theorems

docs/tutorial/interactive.rst

@@ -4,7 +4,7 @@
 Interactive Editing
 ===================
 
-By now, we have seen several examples of how ``Idris``’ dependent type
+By now, we have seen several examples of how Idris’ dependent type
 system can give extra confidence in a function’s correctness by giving
 a more precise description of its intended behaviour in its *type*. We
 have also seen an example of how the type system can help with EDSL
@@ -13,7 +13,7 @@ object language. However, precise types give us more than verification
 of programs — we can also exploit types to help write programs which
 are *correct by construction*.
 
-The ``Idris`` REPL provides several commands for inspecting and
+The Idris REPL provides several commands for inspecting and
 modifying parts of programs, based on their types, such as case
 splitting on a pattern variable, inspecting the type of a
 metavariable, and even a basic proof search mechanism. In this
@@ -121,7 +121,7 @@ according to the same heuristic. If we update the file (using
     vzipWith f [] [] = ?vzipWith_rhs_3
 
 That is, the pattern variable ``ys`` has been split into one case
-``[]``, ``Idris`` having noticed that the other possible case ``y ::
+``[]``, Idris having noticed that the other possible case ``y ::
 ys`` would lead to a unification error.
 
 :addmissing

docs/tutorial/interp.rst

@@ -22,7 +22,7 @@ booleans, and functions, represented by ``Ty``:
     data Ty = TyInt | TyBool | TyFun Ty Ty
 
 We can write a function to translate these representations to a concrete
-``Idris`` type — remember that types are first class, so can be
+Idris type — remember that types are first class, so can be
 calculated just like any other value:
 
 .. code-block:: idris
@@ -176,7 +176,7 @@ environment:
                                              else interp env e
 
 Given this, an interpreter (Listing :ref:`interpdef`) is a function which
-translates an ``Expr`` into a concrete ``Idris`` value with respect to a
+translates an ``Expr`` into a concrete Idris value with respect to a
 specific environment:
 
 .. code-block:: idris
@@ -199,7 +199,7 @@ value:
 Lambdas are more interesting. In this case, we construct a function
 which interprets the scope of the lambda with a new value in the
 environment. So, a function in the object language is translated to an
-``Idris`` function:
+Idris function:
 
 .. code-block:: idris
 
@@ -214,8 +214,8 @@ because of its type:
     interp env (App f s) = interp env f (interp env s)
 
 Operators and interpreters are, again, direct translations into the
-equivalent ``Idris`` constructs. For operators, we apply the function to
-its operands directly, and for ``If``, we apply the ``Idris``
+equivalent Idris constructs. For operators, we apply the function to
+its operands directly, and for ``If``, we apply the Idris
 ``if...then...else`` construct directly.
 
 .. code-block:: idris
@@ -263,7 +263,7 @@ function on user input:
 Here, ``cast`` is an overloaded function which converts a value from
 one type to another if possible. Here, it converts a string to an
 integer, giving 0 if the input is invalid. An example run of this
-program at the ``Idris`` interactive environment is shown in Listing
+program at the Idris interactive environment is shown in Listing
 :ref:`factrun`.
 
 

docs/tutorial/introduction.rst

@@ -35,10 +35,10 @@ following type to the ``app`` function, which concatenates vectors:
 
     app : Vect n a -> Vect m a -> Vect (n + m) a
 
-This tutorial introduces ``Idris``, a general purpose functional
-programming language with dependent types. The goal of the ``Idris``
+This tutorial introduces Idris, a general purpose functional
+programming language with dependent types. The goal of the Idris
 project is to build a dependently typed language suitable for
-verifiable *systems* programming. To this end, ``Idris`` is a compiled
+verifiable *systems* programming. To this end, Idris is a compiled
 language which aims to generate efficient executable code. It also has
 a lightweight foreign function interface which allows easy interaction
 with external ``C`` libraries.
@@ -58,7 +58,7 @@ Example Code
 ------------
 
 This tutorial includes some example code, which has been tested with
-``Idris`` version . The files are available in the ``Idris``
+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

docs/tutorial/miscellany.rst

@@ -48,7 +48,7 @@ this to happen silently. We define ``head`` as follows:
     head : (xs : List a) -> {auto p : isCons xs = True} -> a
     head (x :: xs) = x
 
-The ``auto`` annotation on the implicit argument means that ``Idris``
+The ``auto`` annotation on the implicit argument means that Idris
 will attempt to fill in the implicit argument using the ``trivial``
 tactic, which searches through the context for a proof, and tries to
 solve with ``refl`` if a proof is not found. Now when ``head`` is
@@ -72,7 +72,7 @@ to:
 Implicit conversions
 --------------------
 
-``Idris`` supports the creation of *implicit conversions*, which allow
+Idris supports the creation of *implicit conversions*, which allow
 automatic conversion of values from one type to another when required to
 make a term type correct. This is intended to increase convenience and
 reduce verbosity. A contrived but simple example is the following:
@@ -101,7 +101,7 @@ beyond the scope of this tutorial.
 Literate programming
 --------------------
 
-Like Haskell, ``Idris`` supports *literate* programming. If a file has
+Like Haskell, Idris supports *literate* programming. If a file has
 an extension of ``.lidr`` then it is assumed to be a literate file. In
 literate programs, everything is assumed to be a comment unless the line
 begins with a greater than sign ``>``, for example:
@@ -124,7 +124,7 @@ Foreign function calls
 
 For practical programming, it is often necessary to be able to use
 external libraries, particularly for interfacing with the operating
-system, file system, networking, *et cetera*. ``Idris`` provides a
+system, file system, networking, *et cetera*. Idris provides a
 lightweight foreign function interface for achieving this, as part of
 the prelude. For this, we assume a certain amount of knowledge of C and
 the ``gcc`` compiler. First, we define a datatype which describes the
@@ -136,7 +136,7 @@ external types we can handle:
 
 Each of these corresponds directly to a C type. Respectively: ``int``,
 ``double``, ``char``, ``char*``, ``void*`` and ``void``. There is also a
-translation to a concrete ``Idris`` type, described by the following
+translation to a concrete Idris type, described by the following
 function:
 
 .. code-block:: idris
@@ -150,7 +150,7 @@ function:
     interpFTy FUnit   = ()
 
 A foreign function is described by a list of input types and a return
-type, which can then be converted to an ``Idris`` type:
+type, which can then be converted to an Idris type:
 
 .. code-block:: idris
 
@@ -170,7 +170,7 @@ A foreign function is assumed to be impure, so ``ForeignTy`` builds an
 We build a call to a foreign function by giving the name of the
 function, a list of argument types and the return type. The built in
 construct ``mkForeign`` converts this description to a function callable
-by ``Idris``:
+by Idris:
 
 .. code-block:: idris
 
@@ -194,7 +194,7 @@ Include and linker directives
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Foreign function calls are translated directly to calls to C functions,
-with appropriate conversion between the ``Idris`` representation of a
+with appropriate conversion between the Idris representation of a
 value and the C representation. Often this will require extra libraries
 to be linked in, or extra header and object files. This is made possible
 through the following directives:
@@ -303,7 +303,7 @@ are available in an external collection [1]_.
 C Target
 --------
 
-The default target of ``Idris`` is C. Compiling via :
+The default target of Idris is C. Compiling via :
 
 ::
 
@@ -343,7 +343,7 @@ is shown below :
 JavaScript Target
 -----------------
 
-``Idris`` is capable of producing *JavaScript* code that can be run in a
+Idris is capable of producing *JavaScript* code that can be run in a
 browser as well as in the *NodeJS* environment or alike. One can use the
 FFI to communicate with the *JavaScript* ecosystem.
 
@@ -360,7 +360,7 @@ that is tailored for running in the browser issue the following command:
 The resulting file can be embedded into your HTML just like any other
 *JavaScript* code.
 
-Generating code for *NodeJS* is slightly different. ``Idris`` outputs a
+Generating code for *NodeJS* is slightly different. Idris outputs a
 *JavaScript* file that can be directly executed via ``node``.
 
 ::
@@ -421,7 +421,7 @@ the way we use ``f`` in ``twice``, it would be more obvious if
 
 The *JavaScript* FFI is able to understand functions as arguments when
 you give it something of type ``FFunction``. The following example code
-calls ``twice`` in *JavaScript* and returns the result to our ``Idris``
+calls ``twice`` in *JavaScript* and returns the result to our Idris
 program:
 
 .. code-block:: idris
@@ -450,7 +450,7 @@ via FFI which are stored in external files. The *JavaScript* and
 mind that *JavaScript* and *NodeJS* are handled as different code
 generators, therefore you will have to state which one you want to
 target. This means that you can include different files for *JavaScript*
-and *NodeJS* in the same ``Idris`` source file.
+and *NodeJS* in the same Idris source file.
 
 So whenever you want to add an external *JavaScript* file you can do
 this like so:
@@ -488,13 +488,13 @@ This directive compiles into the following *JavaScript*
 Shrinking down generated *JavaScript*
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-``Idris`` can produce very big chunks of *JavaScript* code. However, the
+Idris can produce very big chunks of *JavaScript* code. However, the
 generated code can be minified using the ``closure-compiler`` from
 Google. Any other minifier is also suitable but ``closure-compiler``
 offers advanced compilation that does some aggressive inlining and code
-elimination. ``Idris`` can take full advantage of this compilation mode
+elimination. Idris can take full advantage of this compilation mode
 and it’s highly recommended to use it when shipping a *JavaScript*
-application written in ``Idris``.
+application written in Idris.
 
 Cumulativity
 ------------
@@ -509,7 +509,7 @@ types themselves have types. For example:
     *universe> :t Vect
     Vect : Nat -> Type -> Type
 
-But what about the type of ``Type``? If we ask ``Idris`` it reports
+But what about the type of ``Type``? If we ask Idris it reports
 
 ::