Refactored the docs directory for latest sphinx_rtd_theme.

Source and build directory are seperate.
References and footnotes are named.
Other than that, tried to do no changes in the docs.
Fixed multi label in proofs-index.
Fixed most of the warnings in make html.
HTML and PDF are building.

docs/LICENSE

@@ -0,0 +1,10 @@
+#+TITLE: Licensing Information
+
+The documentation for Idris has been published under the Creative
+Commons CC0 License. As such to the extent possible under law, /The
+Idris Community/ has waived all copyright and related or neighboring
+rights to Documentation for Idris.
+
+More information concerning the CC0 can be found online at:
+
+    https://creativecommons.org/publicdomain/zero/1.0/

docs/Makefile

@@ -0,0 +1,20 @@
+# Minimal makefile for Sphinx documentation
+#
+
+# You can set these variables from the command line, and also
+# from the environment for the first two.
+SPHINXOPTS    ?=
+SPHINXBUILD   ?= sphinx-build
+SOURCEDIR     = source
+BUILDDIR      = build
+
+# Put it first so that "make" without argument is like "make help".
+help:
+	@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
+
+.PHONY: help Makefile
+
+# Catch-all target: route all unknown targets to Sphinx using the new
+# "make mode" option.  $(O) is meant as a shortcut for $(SPHINXOPTS).
+%: Makefile
+	@$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)

docs/README.md

@@ -0,0 +1,56 @@
+# Documentation for the Idris Language.
+
+
+This manual has been prepared using ReStructured Text and the [Sphinx Documentation Generator](https://www.sphinx-doc.org) for future inclusion on [Read The Docs](https://readthedocs.org).
+
+## Dependencies
+
+To build the manual the following dependencies must be met. We assume that you have standard build automation tools already install i.e. `make`.
+
+### Sphinx-Doc
+
+Python should be installed by default on most systems.
+Sphinx can be installed either through your hosts package manager or using pip/easy_install.
+Recommended way is to use virtual environment for building documentation.
+
+*Note* [ReadTheDocs](https://readthedocs.org) works with Sphinx
+ `v1.2.2`. If you install a more recent version of sphinx then
+ 'incorrectly' marked up documentation may get passed the build system
+ of readthedocs and be ignored. In the past we had several code-blocks
+ disappear because of that.
+
+The ReadTheDocs theme can be installed in virtual environment using pip as follows:
+
+```sh
+python3 -m venv idris2docs_venv
+source idris2docs_venv/bin/activate
+pip install --upgrade pip
+pip install sphinx_rtd_theme
+```
+
+### LaTeX
+
+LaTeX can be install either using your systems package manager or direct from TeXLive.
+
+
+## Build Instructions
+
+```sh
+cd docs
+make html
+make latexpdf
+```
+
+## Contributing
+
+The documentation for Idris has been published under the Creative
+Commons CC0 License. As such to the extent possible under law, /The
+Idris Community/ has waived all copyright and related or neighboring
+rights to Documentation for Idris.
+
+More information concerning the CC0 can be found online at:
+
+    https://creativecommons.org/publicdomain/zero/1.0/
+
+
+When contributing material to the manual please bear in mind that the work will be licensed as above.

docs/make.bat

@@ -0,0 +1,35 @@
+@ECHO OFF
+
+pushd %~dp0
+
+REM Command file for Sphinx documentation
+
+if "%SPHINXBUILD%" == "" (
+	set SPHINXBUILD=sphinx-build
+)
+set SOURCEDIR=source
+set BUILDDIR=build
+
+if "%1" == "" goto help
+
+%SPHINXBUILD% >NUL 2>NUL
+if errorlevel 9009 (
+	echo.
+	echo.The 'sphinx-build' command was not found. Make sure you have Sphinx
+	echo.installed, then set the SPHINXBUILD environment variable to point
+	echo.to the full path of the 'sphinx-build' executable. Alternatively you
+	echo.may add the Sphinx directory to PATH.
+	echo.
+	echo.If you don't have Sphinx installed, grab it from
+	echo.http://sphinx-doc.org/
+	exit /b 1
+)
+
+%SPHINXBUILD% -M %1 %SOURCEDIR% %BUILDDIR% %SPHINXOPTS% %O%
+goto end
+
+:help
+%SPHINXBUILD% -M help %SOURCEDIR% %BUILDDIR% %SPHINXOPTS% %O%
+
+:end
+popd

docs/source/app/index.rst

@@ -0,0 +1,49 @@
+.. _app-index:
+
+################################
+Structuring Idris 2 Applications
+################################
+
+A tutorial on structuring Idris 2 applications using ``Control.App``.
+
+.. note::
+
+   The documentation for Idris has been published under the Creative
+   Commons CC0 License. As such to the extent possible under law, *The
+   Idris Community* has waived all copyright and related or neighboring
+   rights to Documentation for Idris.
+
+   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+
+.. toctree::
+   :maxdepth: 1
+
+Idris applications have ``main : IO ()`` as an entry point.  A type ``IO a`` is
+a description of interactive actions which produce a value of type ``a``. This
+is fine for primitives, but ``IO`` does not support exceptions so we have to be
+explicit about how an operation handles failure. Also, if we do
+want to support exceptions, we also want to explain how exceptions and linearity
+(see Section :ref:`sect-multiplicities`) interact.
+
+In this tutorial, we describe a parameterised type ``App`` and a related
+parameterised type ``App1``, which together allow us to structure larger
+applications, taking into account both exceptions and linearity. The aims of
+``App`` and ``App1`` are that they should:
+
+* make it possible to express what interactions a function does, in its type,
+  without too much notational overhead.
+* have little or no performance overhead compared to writing in *IO*.
+* be compatible with other libraries and techniques for describing effects,
+  such as algebraic effects or monad transformers.
+* be sufficiently easy to use and performant that it can be the basis of
+  *all* libraries that make foreign function calls, much as *IO*
+  is in Idris 1 and Haskell
+* be compatible with linear types, meaning that they should express whether a
+  section of code is linear (guaranteed to execute exactly once without
+  throwing an exception) or whether it might throw an exception.
+
+We begin by introducing ``App``, with some small example
+programs, then show how to extend it with exceptions, state, and other
+interfaces.
+
+[To be continued...]

docs/source/backends/chez.rst

@@ -0,0 +1,47 @@
+**************************
+Chez Scheme Code Generator
+**************************
+
+The Chez Scheme code generator is the default, or it can be accessed via a REPL
+command:
+
+::
+
+    Main> :set cg chez
+
+By default, therefore, to run Idris programs you will need to install
+`Chez Scheme <https://www.scheme.com/>`_. Chez Scheme is open source, and
+available via most OS package managers.
+
+You can compile an expression ``expr`` of type ``IO ()`` to an executable as
+follows, at the REPL:
+
+::
+
+    Main> :c execname expr
+
+...where ``execname`` is the name of the executable file. This will generate
+the following:
+
+* A shell script ``build/exec/execname`` which invokes the program
+* A subdirectory ``build/exec/execname_app`` which contains all the data necessary
+  to run the program. This includes the Chez Scheme source (``execname.ss``),
+  the compiled Chez Scheme code (``execname.so``) and any shared libraries needed
+  for foreign function definitions.
+
+The executable ``execname`` is relocatable to any subdirectory, provided that
+``execname_app`` is also in the same subdirectory.
+
+You can also execute an expression directly:
+
+::
+
+    Main> :exec expr
+
+Again, ``expr`` must have type ``IO ()``. This will generate a temporary
+executable script ``_tmpchez`` in the ``build/exec`` directory, and execute
+that.
+
+Chez Scheme is the default code generator, so if you invoke ``idris2`` with the
+``-o execname`` flag, it will generate an executable script
+``build/exec/execname``, again with support files in ``build/exec/execname_app``.

docs/source/backends/index.rst

@@ -0,0 +1,49 @@
+.. _sect-execs:
+
+************************
+Compiling to Executables
+************************
+
+.. note::
+
+   The documentation for Idris has been published under the Creative
+   Commons CC0 License. As such to the extent possible under law, *The
+   Idris Community* has waived all copyright and related or neighboring
+   rights to Documentation for Idris.
+
+   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+
+Idris 2 (the language) is designed to be independent of any specific code
+generator. Still, since the point of writing a program is to be able to run it,
+it's important to know how to do so! By default, Idris compiles to executables
+via `Chez Scheme <https://www.scheme.com/>`_.
+
+You can compile to an executable as follows, at the REPL:
+
+::
+
+     Main> :c execname expr
+
+...where ``execname`` is the name of the executable file to generate, and
+``expr`` is the Idris expression which will be executed. ``expr`` must have
+type ``IO ()``. This will result in an executable file ``execname``, in a
+directory ``build/exec``, relative to the current working directory.
+
+You can also execute expressions directly:
+
+::
+
+    Main> :exec expr
+
+Again, ``expr`` must have type ``IO ()``.
+
+There are two code generators provided in Idris 2, and (later) there will be
+a system for plugging in new code generators for a variety of targets. The
+default is to compile via Chez Scheme, with an alternative via Racket.
+
+.. toctree::
+   :maxdepth: 1
+
+   chez
+   racket
+

docs/source/backends/racket.rst

@@ -0,0 +1,11 @@
+*********************
+Racket Code Generator
+*********************
+
+The Racket code generator is accessed via a REPL command:
+
+::
+
+    Main> :set cg racket
+
+[More details TODO]

docs/source/conf.py

@@ -0,0 +1,298 @@
+# Configuration file for the Sphinx documentation builder.
+#
+# Idris Manual documentation build configuration file, created by 
+# sphinx-quickstart on Apr 13, 2020.
+#
+# This file is execfile()d with the current directory set to its
+# containing dir.
+#
+# This file only contains a selection of the most common options. For a full
+# list see the documentation:
+# https://www.sphinx-doc.org/en/master/usage/configuration.html
+
+# -- Path setup --------------------------------------------------------------
+
+# If extensions (or modules to document with autodoc) are in another directory,
+# add these directories to sys.path here. If the directory is relative to the
+# documentation root, use os.path.abspath to make it absolute, like shown here.
+#
+import os
+import sys
+import sphinx_rtd_theme
+# sys.path.insert(0, os.path.abspath('.'))
+
+
+# -- Project information -----------------------------------------------------
+
+# General information about the project.
+project = 'Idris2'
+copyright = '2020, The Idris Community'
+author = 'The Idris Community'
+
+# The short X.Y version.
+version = '0.0'
+
+# The full version, including alpha/beta/rc tags
+release = '0.0'
+
+
+# -- General configuration ---------------------------------------------------
+
+# Add any Sphinx extension module names here, as strings. They can be
+# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
+# ones.
+extensions = [
+    'sphinx.ext.todo',
+#    'sphinx.ext.pngmath', # imgmath is not supported on readthedocs.
+    'sphinx.ext.ifconfig',
+    "sphinx_rtd_theme",
+]
+
+# Add any paths that contain templates here, relative to this directory.
+templates_path = ['_templates']
+
+# List of patterns, relative to source directory, that match files and
+# directories to ignore when looking for source files.
+# This pattern also affects html_static_path and html_extra_path.
+exclude_patterns = []
+
+
+# -- Options for HTML output -------------------------------------------------
+
+# The master toctree document.
+master_doc = 'index'
+
+# The theme to use for HTML and HTML Help pages.  See the documentation for
+# a list of builtin themes.
+# # Read The Docs Themes specific settings
+html_theme = 'sphinx_rtd_theme'
+html_theme_options = {
+    'display_version': True,
+    'prev_next_buttons_location': 'bottom'
+}
+
+
+
+
+# Add any paths that contain custom static files (such as style sheets) here,
+# relative to this directory. They are copied after the builtin static files,
+# so a file named "default.css" will overwrite the builtin "default.css".
+html_static_path = ['_static']
+
+# Output file base name for HTML help builder.
+htmlhelp_basename = 'IdrisManualdoc'
+
+# -- Options for LaTeX output ---------------------------------------------
+
+latex_title_page = r'''
+\begin{titlepage}
+    \vspace*{\fill}
+    \begin{center}
+        \includegraphics[width=0.25\textwidth]{idris-512x512.png}\par
+        \vspace{1cm}
+        {\huge\sffamily\bfseries \makeatletter\@title\makeatother\par}
+        \vspace{1cm}
+        {\Large Version \version\par}
+    \end{center}
+    \vspace*{\fill}
+\end{titlepage}
+'''
+
+latex_elements = {
+# The paper size ('letterpaper' or 'a4paper').
+'papersize': 'a4paper',
+
+'fontpkg': '',
+'inputenc': '',
+'utf8extra': '',
+'releasename': 'Version',
+
+# The font size ('10pt', '11pt' or '12pt').
+'pointsize': '10pt',
+
+# Additional stuff for the LaTeX preamble.
+'preamble': r'''
+\usepackage{lmodern}
+\usepackage[T1]{fontenc}
+\usepackage[utf8x]{inputenc}
+\usepackage{titlesec}
+%
+\usepackage{fancyhdr}
+\fancypagestyle{plain}{%
+  \renewcommand{\headrulewidth}{0pt}%
+  \fancyhf{}%
+  \fancyfoot[C]{\textsf{\thepage}}
+}
+\pagestyle{fancy}
+\fancyhf{}
+\fancyhead[LE,RO]{\textsf{\bfseries{v\version}}}
+\fancyhead[LO,RE]{\textsf{\bfseries\leftmark}}
+%\fancyhead[LO]{\textsf{\bfseries{\leftmark}}}
+%\fancyhead[RO]{\textsf{\bfseries{v\version}}}
+%\fancyhead[RE]{\textsf{\bfseries{\leftmark}}}
+%\fancyhead[LE]{\textsf{\bfseries{v\version}}}
+\fancyfoot[C]{\textsf{\thepage}}
+\renewcommand{\footrulewidth}{0pt}
+\renewcommand{\headrulewidth}{0pt}
+%
+\usepackage[font={small,it}]{caption}
+\titleformat{\section}
+  {\normalfont\sffamily\Large\bfseries\color{black}}
+  {\thesection}{1em}{}
+\titleformat{\subsection}
+  {\sffamily\large\bfseries\color{black}}
+  {\thesubsection}{1em}{}
+\titleformat{\subsubsection}
+  {\sffamily\normalsize\bfseries\color{black}}
+  {\thesubsubsection}{1em}{}
+\titleformat{\paragraph}{\normalfont\normalsize\slshape}{\theparagraph}{1em}{}
+\setlength{\parskip}{1em}
+%
+\hypersetup{colorlinks = false}
+\definecolor{VerbatimBorderColor}{rgb}{1,1,1}
+''',
+
+'maketitle': latex_title_page,
+'tableofcontents': "\\tableofcontents"
+# Latex figure (float) alignment
+#'figure_align': 'htbp',
+}
+
+# Grouping the document tree into LaTeX files. List of tuples
+# (source start file, target name, title,
+#  author, documentclass [howto, manual, or own class]).
+latex_documents = [
+  ('index',  'idris-documentation-complete.tex',  u'Documentation for the Idris Language',    u'The Idris Community', 'report'),
+   ('tutorial/index',  'idris-tutorial.tex',  u'The Idris Tutorial',    u'The Idris Community', 'howto'),
+]
+
+
+latex_show_pagerefs = True
+latex_show_url = 'footnote'
+
+# The name of an image file (relative to this directory) to place at the top of
+# the title page.
+latex_logo = '../../icons/idris-512x512.png'
+
+# For "manual" documents, if this is true, then toplevel headings are parts,
+# not chapters.
+#latex_use_parts = True
+
+# If true, show page references after internal links.
+#latex_show_pagerefs = False
+
+# If true, show URL addresses after external links.
+#latex_show_urls = False
+
+# Documents to append as an appendix to all manuals.
+#latex_appendices = []
+
+# If false, no module index is generated.
+#latex_domain_indices = True
+
+
+# -- Options for manual page output ---------------------------------------
+
+# One entry per manual page. List of tuples
+# (source start file, name, description, authors, manual section).
+man_pages = [
+    (master_doc, 'idrismanual', u'Idris Manual Documentation',
+     [author], 1)
+]
+
+# If true, show URL addresses after external links.
+#man_show_urls = False
+
+
+# -- Options for Texinfo output -------------------------------------------
+
+# Grouping the document tree into Texinfo files. List of tuples
+# (source start file, target name, title, author,
+#  dir menu entry, description, category)
+texinfo_documents = [
+  (master_doc, 'IdrisManual', u'Idris Manual Documentation',
+   author, 'IdrisManual', 'One line description of project.',
+   'Miscellaneous'),
+]
+
+# Documents to append as an appendix to all manuals.
+#texinfo_appendices = []
+
+# If false, no module index is generated.
+#texinfo_domain_indices = True
+
+# How to display URL addresses: 'footnote', 'no', or 'inline'.
+#texinfo_show_urls = 'footnote'
+
+# If true, do not generate a @detailmenu in the "Top" node's menu.
+#texinfo_no_detailmenu = False
+
+
+# -- Options for Epub output ----------------------------------------------
+
+# Bibliographic Dublin Core info.
+epub_title = project
+epub_author = author
+epub_publisher = author
+epub_copyright = copyright
+
+# The basename for the epub file. It defaults to the project name.
+#epub_basename = project
+
+# The HTML theme for the epub output. Since the default themes are not optimized
+# for small screen space, using the same theme for HTML and epub output is
+# usually not wise. This defaults to 'epub', a theme designed to save visual
+# space.
+#epub_theme = 'epub'
+
+# The language of the text. It defaults to the language option
+# or 'en' if the language is not set.
+#epub_language = ''
+
+# The scheme of the identifier. Typical schemes are ISBN or URL.
+#epub_scheme = ''
+
+# The unique identifier of the text. This can be a ISBN number
+# or the project homepage.
+#epub_identifier = ''
+
+# A unique identification for the text.
+#epub_uid = ''
+
+# A tuple containing the cover image and cover page html template filenames.
+#epub_cover = ()
+
+# A sequence of (type, uri, title) tuples for the guide element of content.opf.
+#epub_guide = ()
+
+# HTML files that should be inserted before the pages created by sphinx.
+# The format is a list of tuples containing the path and title.
+#epub_pre_files = []
+
+# HTML files shat should be inserted after the pages created by sphinx.
+# The format is a list of tuples containing the path and title.
+#epub_post_files = []
+
+# A list of files that should not be packed into the epub file.
+epub_exclude_files = ['search.html']
+
+# The depth of the table of contents in toc.ncx.
+#epub_tocdepth = 3
+
+# Allow duplicate toc entries.
+#epub_tocdup = True
+
+# Choose between 'default' and 'includehidden'.
+#epub_tocscope = 'default'
+
+# Fix unsupported image types using the Pillow.
+#epub_fix_images = False
+
+# Scale large images.
+#epub_max_image_width = 0
+
+# How to display URL addresses: 'footnote', 'no', or 'inline'.
+#epub_show_urls = 'inline'
+
+# If false, no index is generated.
+#epub_use_index = True

docs/source/faq/faq.rst

@@ -0,0 +1,12 @@
+**************************
+Frequently Asked Questions
+**************************
+
+Can Idris 2 compile itself?
+===========================
+
+Not yet. Although it is written in Idris, there are several changes to the
+language which are not fully backwards compatible (see Section
+:ref:`updates-index`) so, although we hope to get there fairly soon - especially
+since we are resisting using any of the more sophisticated language features -
+it's not automatically the case that it will be able to compile itself.

docs/source/ffi/ffi.rst

@@ -0,0 +1,411 @@
+************
+FFI Overview
+************
+
+Foreign functions are declared with the ``%foreign`` directive, which takes the
+following general form:
+
+.. code-block:: idris
+
+    %foreign [specifiers]
+    name : t
+
+The specifier is an Idris ``String`` which says in which language the foreign
+function is written, what it's called, and where to find it. There may be more
+than one specifier, and a code generator is free to choose any specifier it
+understands - or even ignore the specifiers completely and use their own
+approach. In general, a specifier has the form "Language:name,library". For
+example, in C:
+
+.. code-block:: idris
+
+    %foreign "C:puts,libc"
+    puts : String -> PrimIO Int
+
+It is up to specific code generators to decide how to locate the function and
+the library. In this document, we will assume the default Chez Scheme code
+generator (the examples also work with the Racket code generator) and that the
+foreign language is C.
+
+Example
+-------
+
+As a running example, we are going to work with a small C file. Save the
+following content to a file ``smallc.c``
+
+::
+
+    #include <stdio.h>
+
+    int add(int x, int y) {
+        return x+y;
+    }
+
+    int addWithMessage(char* msg, int x, int y) {
+        printf("%s: %d + %d = %d\n", msg, x, y, x+y);
+        return x+y;
+    }
+
+Then, compile it to a shared library with::
+
+    cc -shared smallc.c -o libsmall.so
+
+We can now write an Idris program which calls each of these. First, we'll
+write a small program which uses ``add`` to add two integers:
+
+.. code-block:: idris
+
+    %foreign "C:add,libsmall"
+    add : Int -> Int -> Int
+  
+    main : IO ()
+    main = printLn (add 70 24)
+
+The ``%foreign`` declaration states that ``add`` is written in C, with the
+name ``add`` in the library ``libsmall``. As long as the run time is able
+to locate ``libsmall.so`` (in practice it looks in the current directory and
+the system library paths) we can run this at the REPL:
+
+::
+
+    Main> :exec main
+    94
+
+Note that it is the programmer's responsibility to make sure that the
+Idris function and C function have corresponding types. There is no way for
+the machine to check this! If you get it wrong, you will get unpredictable
+behaviour.
+
+Since ``add`` has no side effects, we've given it a return type of ``Int``.
+But what if the function has some effect on the outside world, like
+``addWithMessage``? In this case, we use ``PrimIO Int`` to say that it
+returns a primitive IO action:
+
+.. code-block:: idris
+
+    %foreign "C:addWithMessage,libsmall"
+    prim_addWithMessage : String -> Int -> Int -> PrimIO Int
+
+Internally, ``PrimIO Int`` is a function which takes the current (linear)
+state of the world, and returns an ``Int`` with an updated state of the world.
+We can convert this into an ``IO`` action using ``primIO``:
+
+.. code-block:: idris
+
+    primIO : PrimIO a -> IO a
+
+So, we can extend our program as follows:
+
+.. code-block:: idris
+
+  addWithMessage : String -> Int -> Int -> IO Int
+  addWithMessage s x y = primIO $ prim_addWithMessage s x y
+  
+  main : IO ()
+  main
+      = do printLn (add 70 24)
+           addWithMessage "Sum" 70 24
+           pure ()
+
+It is up to the programmer to declare which functions are pure, and which have
+side effects, via ``PrimIO``. Executing this gives:
+
+::
+
+    Main> :exec main
+    94
+    Sum: 70 + 24 = 94
+
+We have seen two specifiers for foreign functions:
+
+.. code-block:: idris
+
+    %foreign "C:add,libsmall"
+    %foreign "C:addWithMessage,libsmall"
+
+These both have the same form: ``"C:[name],libsmall"`` so instead of writing
+the concrete ``String``, we write a function to compute the specifier, and
+use that instead:
+
+.. code-block:: idris
+
+    libsmall : String -> String
+    libsmall fn = "C:" ++ fn ++ ",libsmall"
+
+    %foreign (libsmall "add")
+    add : Int -> Int -> Int
+
+    %foreign (libsmall "addWithMessage")
+    prim_addWithMessage : String -> Int -> Int -> PrimIO Int
+
+.. _sect-ffi-string:
+
+Primitive FFI Types
+-------------------
+
+The types which can be passed to and returned from foreign functions are
+restricted to those which it is reasonable to assume any back end can handle.
+In practice, this means most primitive types, and a limited selection of
+others.  Argument types can be any of the following primitives:
+
+* ``Int``
+* ``Char``
+* ``Double`` (as ``double`` in C)
+* ``String`` (as ``char*`` in C)
+* ``Ptr t`` and ``AnyPtr`` (both as ``void*`` in C)
+
+Return types can be any of the above, plus:
+
+* ``()``
+* ``PrimIO t``, where ``t`` is a valid return type other than a ``PrimIO``.
+
+Handling ``String`` leads to some complications, for a number of reasons:
+
+* Strings can have multiple encodings. In the Idris run time, Strings are
+  encoded as UTF-8, but C makes no assumptions.
+* It is not always clear who is responsible for freeing a ``String`` allocated
+  by a C function.
+* In C, strings can be ``NULL``, but Idris strings always have a value.
+
+So, when passing ``String`` to and from C, remember the following:
+
+* A ``char*`` returned by a C function will be copied to the Idris heap, and
+  the Idris run time immediately calls ``free`` with the returned ``char*``.
+* If a ``char*`` might be ``NULL`` in ``C``, use ``Ptr String`` rather than
+  ``String``.
+
+When using ``Ptr String``, the value will be passed as a ``void*``, and
+therefore not accessible directly by Idris code. This is to protect against
+accidentally trying to use ``NULL`` as a ``String``. You can nevertheless
+work with them and convert to ``String`` via foreign functions of the following
+form:
+
+::
+
+    char* getString(void *p) {
+        return (char*)p;
+    }
+
+    void* mkString(char* str) {
+        return (void*)str;
+    }
+
+    int isNullString(void* str) {
+        return str == NULL;
+    }
+
+For an example, see the sample :ref:`sect-readline` bindings.
+
+Additionally, foreign functions can take *callbacks*, and take and return
+C ``struct`` pointers.
+
+.. _sect-callbacks:
+
+Callbacks
+---------
+
+It is often useful in C for a function to take a *callback*, that is a function
+which is called after doing some work. For example, we can write a function
+which takes a callback that takes a ``char*`` and an ``int`` and returns a
+``char*``, in C, as follows (added to ``smallc.c`` above):
+
+::
+
+    typedef char*(*StringFn)(char*, int);
+
+    char* applyFn(char* x, int y, StringFn f) {
+        printf("Applying callback to %s %d\n", x, y);
+        return f(x, y);
+    }
+
+Then, we can access this from Idris by declaring it as a ``%foreign``
+function and wrapping it in ``IO``, with the C function calling the Idris
+function as the callback:
+
+.. code-block:: idris
+
+    %foreign (libsmall "applyFn")
+    prim_applyFn : String -> Int -> (String -> Int -> String) -> PrimIO String
+    
+    applyFn : String -> Int -> (String -> Int -> String) -> IO String
+    applyFn c i f = primIO $ prim_applyFn c i f
+
+For example, we can try this as follows:
+
+.. code-block:: idris
+
+    pluralise : String -> Int -> String
+    pluralise str x
+        = show x ++ " " ++
+                 if x == 1
+                    then str
+                    else str ++ "s"
+    
+    main : IO ()
+    main
+        = do str1 <- applyFn "Biscuit" 10 pluralise
+             putStrLn str1
+             str2 <- applyFn "Tree" 1 pluralise
+             putStrLn str2
+
+As a variant, the callback could have a side effect:
+
+.. code-block:: idris
+
+    %foreign (libsmall "applyFn")
+    prim_applyFnIO : String -> Int -> (String -> Int -> PrimIO String) ->
+                     PrimIO String
+  
+This is a little more fiddly to lift to an ``IO`` function, due to the callback,
+but we can do so using ``toPrim : IO a -> PrimIO a``:
+  
+.. code-block:: idris
+
+    applyFnIO : String -> Int -> (String -> Int -> IO String) -> IO String
+    applyFnIO c i f = primIO $ prim_applyFnIO c i (\s, i => toPrim $ f s i)
+  
+For example, we can extend the above ``pluralise`` example to print a message
+in the callback:
+
+.. code-block:: idris
+
+    pluralise : String -> Int -> IO String
+    pluralise str x
+        = do putStrLn "Pluralising"
+             pure $ show x ++ " " ++
+                    if x == 1
+                       then str
+                       else str ++ "s"
+    
+    main : IO ()
+    main
+        = do str1 <- applyFnIO "Biscuit" 10 pluralise
+             putStrLn str1
+             str2 <- applyFnIO "Tree" 1 pluralise
+             putStrLn str2
+
+Structs
+-------
+
+Many C APIs pass around more complex data structures, as a ``struct``.
+We do not aim to be completely general in the C types we support, because
+this will make it harder to write code which is portable across multiple
+back ends. However, it is still often useful to be able to access a ``struct``
+directly. For example, add the following to the top of ``smallc.c``, and
+rebuild ``libsmall.so``:
+
+::
+
+    #include <stdlib.h>
+
+    typedef struct {
+        int x;
+        int y;
+    } point;
+
+    point* mkPoint(int x, int y) {
+        point* pt = malloc(sizeof(point));
+        pt->x = x;
+        pt->y = y;
+        return pt;
+    }
+
+    void freePoint(point* pt) {
+        free(pt);
+    }
+
+We can define a type for accessing ``point`` in Idris by importing
+``System.FFI`` and using the ``Struct`` type, as follows:
+
+.. code-block:: idris
+
+    Point : Type
+    Point = Struct "point" [("x", Int), ("y", Int)]
+    
+    %foreign (libsmall "mkPoint")
+    mkPoint : Int -> Int -> Point
+    
+    %foreign (libsmall "freePoint")
+    prim_freePoint : Point -> PrimIO ()
+    
+    freePoint : Point -> IO ()
+    freePoint p = primIO $ prim_freePoint p
+
+The ``Point`` type in Idris now corresponds to ``point*`` in C. Fields can
+be read and written using the following, also from ``System.FFI``:
+
+.. code-block:: idris
+
+    getField : Struct s fs -> (n : String) ->
+               FieldType n ty fs => ty
+    setField : Struct s fs -> (n : String) ->
+               FieldType n ty fs => ty -> IO ()
+
+Notice that fields are accessed by name, and must be available in the
+struct, given the constraint ``FieldType n ty fs``, which states that the
+field named ``n`` has type ``ty`` in the structure fields ``fs``.
+So, we can display a ``Point`` as follows by accessing the fields directly:
+
+.. code-block:: idris
+
+    showPoint : Point -> String
+    showPoint pt
+        = let x : Int = getField pt "x"
+              y : Int = getField pt "y" in
+              show (x, y)
+
+And, as a complete example, we can initialise, update, display and
+delete a ``Point`` as follows:
+
+.. code-block:: idris
+
+    main : IO ()
+    main = do let pt = mkPoint 20 30
+              setField pt "x" (the Int 40)
+              putStrLn $ showPoint pt
+              freePoint pt
+
+The field types of a ``Struct`` can be any of the following:
+
+* ``Int``
+* ``Char``
+* ``Double`` (``double`` in C)
+* ``Ptr a`` or ``AnyPtr`` (``void*`` in C)
+* Another ``Struct``, which is a pointer to a ``struct`` in C
+
+Note that this doesn't include ``String`` or function types! This is primarily
+because these aren't directly supported by the Chez back end. However, you can
+use another pointer type and convert. For example, assuming you have, in C:
+
+::
+
+    typedef struct {
+        char* name;
+        point* pt;
+    } namedpoint;
+
+You can represent this in Idris as:
+
+::
+
+    NamedPoint : Type
+    NamedPoint 
+        = Struct "namedpoint" 
+                   [("name", Ptr String),
+                   ("pt", Point)]
+
+That is, using a ``Ptr String`` instead of a ``String`` directly. Then you
+can convert between a ``void*`` and a ``char*`` in C:
+
+::
+
+    char* getString(void *p) {
+        return (char*)p;
+    }
+
+...and use this to convert to a ``String`` in Idris:
+
+.. code-block:: idris
+
+    %foreign (pfn "getString")
+    getString : Ptr String -> String

docs/source/ffi/index.rst

@@ -0,0 +1,30 @@
+**************************
+Foreign Function Interface
+**************************
+
+.. note::
+
+   The documentation for Idris has been published under the Creative
+   Commons CC0 License. As such to the extent possible under law, *The
+   Idris Community* has waived all copyright and related or neighboring
+   rights to Documentation for Idris.
+
+   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+
+Idris 2 is designed to support multiple code generators. The default target is
+Chez Scheme, with a Racket code generator also supported. However, the
+intention is, as with Idris 1, to support multiple targets on multiple platforms,
+including e.g. JavaScript, JVM, .NET, and others yet to be invented.
+This makes the design of a foreign function interface (FFI), which calls
+functions in other languages, a little challenging, since ideally it will
+support all possible targets!
+
+To this end, the Idris 2 FFI aims to be flexible and adaptable, while still
+supporting most common requirements without too much need for "glue" code in
+the foreign language.
+
+.. toctree::
+   :maxdepth: 1
+
+   ffi
+   readline

docs/source/ffi/readline.rst

@@ -0,0 +1,307 @@
+.. _sect-readline:
+
+**********************************
+Example: Minimal Readline Bindings
+**********************************
+
+In this section, we'll see how to create bindings for a C library (the `GNU
+Readline <https://tiswww.case.edu/php/chet/readline/rltop.html>`_ library) in
+Idris, and make them available in a package. We'll only create the most minimal
+bindings, but nevertheless they demonstrate some of the trickier problems in
+creating bindings to a C library, in that they need to handle memory allocation
+of ``String``.
+
+You can find the example in full in the Idris 2 source repository, 
+in `samples/FFI-readline
+<https://github.com/edwinb/Idris2/tree/master/samples/FFI-readline>`_. As a
+minimal example, this can be used as a starting point for other C library
+bindings.
+
+We are going to provide bindings to the following functions in the Readline
+API, available via ``#include <readline/readline.h>``:
+
+::
+
+    char* readline (const char *prompt);
+    void add_history(const char *string);
+
+Additionally, we are going to support tab completion, which in the Readline
+API is achieved by setting a global variable to a callback function
+(see Section :ref:`sect-callbacks`) which explains how to handle the
+completion:
+
+::
+
+    typedef char *rl_compentry_func_t (const char *, int);
+    rl_compentry_func_t * rl_completion_entry_function;
+
+A completion function takes a ``String``, which is the text to complete, and
+an ``Int``, which is the number of times it has asked for a completion so far.
+In Idris, this could be a function ``complete : String -> Int -> IO String``.
+So, for example, if the text so far is ``"id"``, and the possible completions
+are ``idiomatic`` and ``idris``, then ``complete "id" 0`` would produce the
+string ``"idiomatic"`` and ``complete "id" 1`` would produce ``"idris"``.
+
+We will define *glue* functions in a C file ``idris_readline.c``, which compiles
+to a shared object ``libidrisreadline``, so we write a function for locating
+the C functions:
+
+.. code-block:: idris
+
+    rlib : String -> String
+    rlib fn = "C:" ++ fn ++ ",libidrisreadline"
+
+Each of the foreign bindings will have a ``%foreign`` specifier which locates
+functions via ``rlib``.
+
+Basic behaviour: Reading input, and history
+-------------------------------------------
+
+We can start by writing a binding for ``readline`` directly. It's interactive,
+so needs to return a ``PrimIO``:
+
+.. code-block:: idris
+
+    %foreign (rlib "readline")
+    prim_readline : String -> PrimIO String
+
+Then, we can write an ``IO`` wrapper:
+
+.. code-block:: idris
+
+    readline : String -> IO String
+    readline prompt = primIO $ readline prompt
+
+Unfortunately, this isn't quite good enough! The C ``readline`` function
+returns a ``NULL`` string if there is no input due to encountering an
+end of file. So, we need to handle that - if we don't, we'll get a crash
+on encountering end of file (remember: it's the Idris programmer's responsibility
+to give an appropriate type to the C binding!)
+
+Instead, we need to use a ``Ptr`` to say that it might be a ``NULL``
+pointer (see Section :ref:`sect-ffi-string`):
+
+.. code-block:: idris
+
+    %foreign (rlib "readline")
+    prim_readline : String -> PrimIO (Ptr String)
+
+We also need to provide a way to check whether the returned ``Ptr String`` is 
+``NULL``. To do so, we'll write some glue code to convert back and forth
+between ``Ptr String`` and ``String``, in a file ``idris_readline.c`` and a
+corresponding header ``idris_readline.h``. In ``idris_readline.h`` we have:
+
+::
+
+    int isNullString(void* str); // return 0 if a string in NULL, non zero otherwise
+    char* getString(void* str); // turn a non-NULL Ptr String into a String (assuming not NULL)
+    void* mkString(char* str); // turn a String into a Ptr String
+    void* nullString(); // create a new NULL String
+
+Correspondingly, in ``idris_readline.c``:
+
+::
+
+    int isNullString(void* str) {
+        return str == NULL;
+    }
+
+    char* getString(void* str) {
+        return (char*)str;
+    }
+
+    void* mkString(char* str) {
+        return (void*)str;
+    }
+
+    void* nullString() {
+        return NULL;
+    }
+
+Now, we can use ``prim_readline`` as follows, with a safe API, checking
+whether the result it returns is ``NULL`` or a concrete ``String``:
+
+.. code-block:: idris
+
+    %foreign (rlib "isNullString")
+    prim_isNullString : Ptr String -> Int
+
+    export
+    isNullString : Ptr String -> Bool
+    isNullString str = if prim_isNullString str == 0 then False else True
+
+    export
+    readline : String -> IO (Maybe String)
+    readline s
+        = do mstr <- primIO $ prim_readline s
+             if isNullString mstr
+                then pure $ Nothing
+                else pure $ Just (getString mstr)
+
+We'll need ``nullString`` and ``mkString`` later, for dealing with completions.
+
+Once we've read a string, we'll want to add it to the input history. We can
+provide a binding to ``add_history`` as follows:
+
+.. code-block:: idris
+
+    %foreign (rlib "add_history")
+    prim_add_history : String -> PrimIO ()
+
+    export
+    addHistory : String -> IO ()
+    addHistory s = primIO $ prim_add_history s
+
+In this case, since Idris is in control of the ``String``, we know it's not
+going to be ``NULL``, so we can add it directly.
+
+A small ``readline`` program that reads input, and echoes it, recording input
+history for non-empty inputs, can be written as follows:
+
+.. code-block:: idris
+
+    echoLoop : IO ()
+    echoLoop 
+        = do Just x <- readline "> "
+                  | Nothing => putStrLn "EOF"
+             putStrLn ("Read: " ++ x)
+             when (x /= "") $ addHistory x
+             if x /= "quit"
+                then echoLoop
+                else putStrLn "Done"
+
+This gives us command history, and command line editing, but Readline becomes
+much more useful when we add tab completion. The default tab completion, which
+is available even in the small example above, is to tab complete file names
+in the current working directory. But for any realistic application, we probably
+want to tab complete other commands, such as function names, references to
+local data, or anything that is appropriate for the application.
+
+Completions
+-----------
+
+Readline has a large API, with several ways of supporting tab completion,
+typically involving setting a global variable to an appropriate completion
+function. We'll use the following:
+
+::
+
+    typedef char *rl_compentry_func_t (const char *, int);
+    rl_compentry_func_t * rl_completion_entry_function;
+
+The completion function takes the prefix of the completion, and the number
+of times it has been called so far on this prefix, and returns the next
+completion, or ``NULL`` if there are no more completions. An Idris equivalent
+would therefore have the following type:
+
+.. code-block:: idris
+
+    setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()
+
+The function returns ``Nothing`` if there are no more completions, or
+``Just str`` for some ``str`` if there is another one for the current
+input.
+
+We might hope that it's a matter of defining a function to assign the
+completion function...
+
+::
+
+    void idrisrl_setCompletion(rl_compentry_func_t* fn) {
+        rl_completion_entry_function = fn;
+    }
+
+...then defining the Idris binding, which needs to take into account that
+the Readline library expects ``NULL`` when there are no more completions:
+
+.. code-block:: idris
+
+    %foreign (rlib "idrisrl_setCompletion")
+    prim_setCompletion : (String -> Int -> PrimIO (Ptr String)) -> PrimIO ()
+
+    export
+    setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()
+    setCompletionFn fn
+        = primIO $ prim_setCompletion $ \s, i => toPrim $
+              do mstr <- fn s i
+                 case mstr of
+                      Nothing => pure nullString // need to return a Ptr String to readline!
+                      Just str => pure (mkString str)
+
+So, we turn ``Nothing`` into ``nullString`` and ``Just str`` into ``mkString
+str``. Unfortunately, this doesn't quite work. To see what goes wrong, let's
+try it for the most basic completion function that returns one completion no
+matter what the input:
+
+.. code-block:: idris
+
+    testComplete : String -> Int -> IO (Maybe String)
+    testComplete text 0 = pure $ Just "hamster"
+    testComplete text st = pure Nothing
+
+We'll try this in a small modification of ``echoLoop`` above, setting a
+completion function first:
+
+.. code-block :: idris
+
+    main : IO ()
+    main = do setCompletionFn testComplete
+              echoLoop
+
+We see that there is a problem when we try running it, and hitting TAB before
+entering anything:
+
+::
+
+    Main> :exec main
+    > free(): invalid pointer
+
+The Idris code which sets up the completion is fine, but there is a problem
+with the memory allocation in the C glue code.
+
+This problem arises because we haven't thought carefully enough about which
+parts of our program are responsible for allocating and freeing strings.
+When Idris calls a foreign function that returns a string, it copies the
+string to the Idris heap and frees it immediately. But, if the foreign
+library also frees the string, it ends up being freed twice. This is what's
+happening here: the callback passed to ``prim_setCompletion`` frees the string
+and puts it onto the Idris heap, but Readline also frees the string returned
+by ``prim_setCompletion`` once it has processed it. We can solve this
+problem by writing a wrapper for the completion function which reallocates
+the string, and using that in ``idrisrl_setCompletion`` instead.
+
+::
+
+    rl_compentry_func_t* my_compentry;
+
+    char* compentry_wrapper(const char* text, int i) {
+        char* res = my_compentry(text, i); // my_compentry is an Idris function, so res is on the Idris heap,
+                                           // and freed on return
+        if (res != NULL) {
+            char* comp = malloc(strlen(res)+1); // comp is passed back to readline, which frees it when
+                                                // it is finished with it
+            strcpy(comp, res);
+            return comp;
+        }
+        else {
+            return NULL;
+        }
+    }
+
+    void idrisrl_setCompletion(rl_compentry_func_t* fn) {
+        rl_completion_entry_function = compentry_wrapper;
+        my_compentry = fn; // fn is an Idris function, called by compentry_wrapper
+    }
+
+So, we define the completion function in C, which calls the Idris completion
+function then makes sure the string returned by the Idris function is copied
+to the C heap.
+
+We now have a primitive API that covers the most fundamental features of the
+readline API:
+
+.. code-block:: idris
+
+    readline : String -> IO (Maybe String)
+    addHistory : String -> IO ()
+    setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()

docs/source/index.rst

@@ -0,0 +1,29 @@
+.. Idris Manual documentation master file, created by
+   sphinx-quickstart on Sat Feb 28 20:41:47 2015.
+   You can adapt this file completely to your liking, but it should at least
+   contain the root `toctree` directive.
+
+Documentation for the Idris 2 Language
+======================================
+
+.. note::
+
+   The documentation for Idris 2 has been published under the Creative
+   Commons CC0 License. As such to the extent possible under law, *The
+   Idris Community* has waived all copyright and related or neighboring
+   rights to Documentation for Idris.
+
+   More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
+
+.. toctree::
+   :maxdepth: 1
+
+   tutorial/index
+   backends/index
+   updates/updates
+   typedd/typedd
+   app/index
+   ffi/index
+   proofs/index
+   faq/faq
+   reference/index

docs/source/listing/idris-prompt-helloworld.txt

@@ -0,0 +1,15 @@
+$ idris hello.idr
+     ____    __     _         ___
+    /  _/___/ /____(_)____   |__ \
+    / // __  / ___/ / ___/   __/ /     Version 0.1.0
+  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
+ /___/\__,_/_/  /_/____/   /____/      Type :? for help
+
+Welcome to Idris 2.  Enjoy yourself!
+Main> :t main
+Main.main : IO ()
+Main> :c hello main
+compiling hello.ss with output to hello.so
+File hello.so written
+Main> :q
+Bye for now!

docs/source/listing/idris-prompt-interp.txt

@@ -0,0 +1,11 @@
+$ idris2 interp.idr
+     ____    __     _         ___
+    /  _/___/ /____(_)____   |__ \
+    / // __  / ___/ / ___/   __/ /     Version 0.1.0
+  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
+ /___/\__,_/_/  /_/____/   /____/      Type :? for help
+
+Welcome to Idris 2.  Enjoy yourself!
+Main> :exec main
+Enter a number: 6
+720

docs/source/listing/idris-prompt-start.txt

@@ -0,0 +1,9 @@
+$ idris2
+     ____    __     _         ___
+    /  _/___/ /____(_)____   |__ \
+    / // __  / ___/ / ___/   __/ /     Version 0.1.0
+  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
+ /___/\__,_/_/  /_/____/   /____/      Type :? for help
+
+Welcome to Idris 2.  Enjoy yourself!
+Main>

docs/source/proofs/definitional.rst

@@ -0,0 +1,210 @@
+Before we discuss the details of theorem proving in Idris, we will describe
+some fundamental concepts:
+
+-  Propositions and judgments
+-  Boolean and constructive logic
+-  Curry-Howard correspondence
+-  Definitional and propositional equalities
+-  Axiomatic and constructive approaches
+
+Propositions and Judgments
+==========================
+
+Propositions are the subject of our proofs. Before the proof, we can't
+formally say if they are true or not. If the proof is successful then the
+result is a 'judgment'.  For instance, if the ``proposition`` is,
+
++-------+
+| 1+1=2 |
++-------+
+
+When we prove it, the ``judgment`` is,
+
++------------+
+| 1+1=2 true |
++------------+
+
+Or if the ``proposition`` is,
+
++-------+
+| 1+1=3 |
++-------+
+
+we can't prove it is true, but it is still a valid proposition and perhaps we
+can prove it is false so the ``judgment`` is, 
+
++-------------+
+| 1+1=3 false |
++-------------+
+
+This may seem a bit pedantic but it is important to be careful: in mathematics
+not every proposition is true or false. For instance, a proposition may be
+unproven or even unprovable.
+
+So the logic here is different from the logic that comes from boolean algebra.
+In that case what is not true is false and what is not false is true. The logic
+we are using here does not have this law, the "Law of Excluded Middle", so we
+cannot use it.
+
+A false proposition is taken to be a contradiction and if we have a
+contradiction then we can prove anything, so we need to avoid this. Some
+languages, used in proof assistants, prevent contradictions.
+
+The logic we are using is called constructive (or sometimes intuitional)
+because we are constructing a 'database' of judgments.
+
+Curry-Howard correspondence
+---------------------------
+
+So how do we relate these proofs to Idris programs? It turns out that there is
+a correspondence between constructive logic and type theory. They have the same
+structure and we can switch back and forth between the two notations.
+
+The way that this works is that a proposition is a type so...
+
+.. code-block:: idris
+
+    Main> 1 + 1 = 2
+    2 = 2
+
+    Main> :t 1 + 1 = 2
+    (fromInteger 1 + fromInteger 1) === fromInteger 2 : Type
+
+...is a proposition and it is also a type. The
+following will also produce an equality type:
+
+
+.. code-block:: idris
+
+   Main> 1 + 1 = 3
+   2 = 3
+
+Both of these are valid propositions so both are valid equality types. But how
+do we represent a true judgment? That is, how do we denote 1+1=2 is true but not
+1+1=3?  A type that is true is inhabited, that is, it can be constructed. An
+equality type has only one constructor 'Refl' so a proof of 1+1=2 is
+
+.. code-block:: idris
+
+   onePlusOne : 1+1=2
+   onePlusOne = Refl
+
+Now that we can represent propositions as types other aspects of
+propositional logic can also be translated to types as follows:
+
++----------+-------------------+--------------------------+
+|          | propositions      | example of possible type |
++----------+-------------------+--------------------------+
+| A        | x=y               |                          |
++----------+-------------------+--------------------------+
+| B        | y=z               |                          |
++----------+-------------------+--------------------------+
+| and      | A /\ B            | Pair(x=y,y=z)            |
++----------+-------------------+--------------------------+
+| or       | A \/ B            | Either(x=y,y=z)          |
++----------+-------------------+--------------------------+
+| implies  | A -> B            | (x=y) -> (y=x)           |
++----------+-------------------+--------------------------+
+| for all  | y=z               |                          |
++----------+-------------------+--------------------------+
+| exists   | y=z               |                          |
++----------+-------------------+--------------------------+
+
+
+And (conjunction)
+-----------------
+
+We can have a type which corresponds to conjunction:
+
+.. code-block:: idris
+
+   AndIntro : a -> b -> A a b
+
+There is a built in type called 'Pair'.
+
+Or (disjunction)
+----------------
+
+We can have a type which corresponds to disjunction:
+
+.. code-block:: idris
+
+   data Or : Type -> Type -> Type where
+   OrIntroLeft : a -> A a b
+   OrIntroRight : b -> A a b
+
+There is a built in type called 'Either'.
+
+Definitional and Propositional Equalities
+-----------------------------------------
+
+We have seen that  we can 'prove' a type by finding a way to construct a term.
+In the case of equality types there is only one constructor which is ``Refl``.
+We have also seen that each side of the equation does not have to be identical
+like '2=2'. It is enough that both sides are *definitionally equal* like this:
+
+.. code-block:: idris
+
+   onePlusOne : 1+1=2
+   onePlusOne = Refl
+
+Both sides of this equation normalise to 2 and so Refl matches and the
+proposition is proved.
+
+We don't have to stick to terms; we can also use symbolic parameters so the
+following type checks:
+
+.. code-block:: idris
+
+   varIdentity : m = m
+   varIdentity = Refl
+
+If a proposition/equality type is not definitionally equal but is still true
+then it is *propositionally equal*. In this case we may still be able to prove
+it but some steps in the proof may require us to add something into the terms
+or at least to take some sideways steps to get to a proof.
+
+Especially when working with equalities containing variable terms (inside
+functions) it can be hard to know which equality types are definitionally equal,
+in this example ``plusReducesL`` is *definitionally equal* but ``plusReducesR`` is
+not (although it is *propositionally equal*). The only difference between
+them is the order of the operands.
+
+.. code-block:: idris
+
+   plusReducesL : (n:Nat) -> plus Z n = n
+   plusReducesL n = Refl
+
+   plusReducesR : (n:Nat) -> plus n Z = n
+   plusReducesR n = Refl
+
+Checking ``plusReducesR`` gives the following error:
+
+
+.. code-block:: idris
+
+    Proofs.idr:21:18--23:1:While processing right hand side of Main.plusReducesR at Proofs.idr:21:1--23:1:
+    Can't solve constraint between:
+            plus n Z
+    and
+            n
+
+So why is ``Refl`` able to prove some equality types but not others?
+
+The first answer is that ``plus`` is defined by recursion on its first
+argument. So, when the first argument is ``Z``, it reduces, but not when the
+second argument is ``Z``.
+
+If an equality type can be proved/constructed by using ``Refl`` alone it is known
+as a *definitional equality*. In order to be definitionally equal both sides
+of the equation must normalise to the same value.
+
+So when we type ``1+1`` in Idris it is immediately reduced to 2 because
+definitional equality is built in
+
+.. code-block:: idris
+
+    Main> 1+1
+    2
+
+In the following pages we discuss how to resolve propositional equalities.

docs/source/proofs/index.rst

@@ -0,0 +1,25 @@
+.. _proofs-index:
+
+###############
+Theorem Proving
+###############
+
+A tutorial on theorem proving in Idris 2. 
+
+.. note::
+
+   The documentation for Idris has been published under the Creative
+   Commons CC0 License. As such to the extent possible under law, *The
+   Idris Community* has waived all copyright and related or neighboring
+   rights to Documentation for Idris.
+
+   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+
+.. toctree::
+   :maxdepth: 1
+
+   definitional
+   pluscomm
+   inductive
+   patterns
+   propositional

docs/source/proofs/inductive.rst

@@ -0,0 +1,102 @@
+.. _sect-inductive:
+
+****************
+Inductive Proofs
+****************
+
+Before embarking on proving ``plus_commutes`` in Idris itself, let us
+consider the overall structure of a proof of some property of natural
+numbers. Recall that they are defined recursively, as follows:
+
+.. code-block:: idris
+
+    data Nat : Type where
+         Z : Nat
+         S : Nat -> Nat
+
+A *total* function over natural numbers must both terminate, and cover
+all possible inputs. Idris checks functions for totality by checking that
+all inputs are covered, and that all recursive calls are on
+*structurally smaller* values (so recursion will always reach a base
+case). Recalling ``plus``:
+
+.. code-block:: idris
+
+    plus : Nat -> Nat -> Nat
+    plus Z     m = m
+    plus (S k) m = S (plus k m)
+
+This is total because it covers all possible inputs (the first argument
+can only be ``Z`` or ``S k`` for some ``k``, and the second argument
+``m`` covers all possible ``Nat``) and in the recursive call, ``k``
+is structurally smaller than ``S k`` so the first argument will always
+reach the base case ``Z`` in any sequence of recursive calls.
+
+In some sense, this resembles a mathematical proof by induction (and
+this is no coincidence!). For some property ``P`` of a natural number
+``x``, we can show that ``P`` holds for all ``x`` if:
+
+-  ``P`` holds for zero (the base case).
+
+-  Assuming that ``P`` holds for ``k``, we can show ``P`` also holds for
+   ``S k`` (the inductive step).
+
+In ``plus``, the property we are trying to show is somewhat trivial (for
+all natural numbers ``x``, there is a ``Nat`` which need not have any
+relation to ``x``). However, it still takes the form of a base case and
+an inductive step. In the base case, we show that there is a ``Nat``
+arising from ``plus n m`` when ``n = Z``, and in the inductive step we
+show that there is a ``Nat`` arising when ``n = S k`` and we know we can
+get a ``Nat`` inductively from ``plus k m``. We could even write a
+function capturing all such inductive definitions:
+
+.. code-block:: idris
+
+    nat_induction :
+        (prop : Nat -> Type) ->                -- Property to show
+        (prop Z) ->                            -- Base case
+        ((k : Nat) -> prop k -> prop (S k)) -> -- Inductive step
+        (x : Nat) ->                           -- Show for all x
+        prop x
+    nat_induction prop p_Z p_S Z = p_Z
+    nat_induction prop p_Z p_S (S k) = p_S k (nat_induction prop p_Z p_S k)
+
+Using ``nat_induction``, we can implement an equivalent inductive
+version of ``plus``:
+
+.. code-block:: idris
+
+    plus_ind : Nat -> Nat -> Nat
+    plus_ind n m
+       = nat_induction (\x => Nat)
+                       m                      -- Base case, plus_ind Z m
+                       (\k, k_rec => S k_rec) -- Inductive step plus_ind (S k) m
+                                              -- where k_rec = plus_ind k m
+                       n
+
+To prove that ``plus n m = plus m n`` for all natural numbers ``n`` and
+``m``, we can also use induction. Either we can fix ``m`` and perform
+induction on ``n``, or vice versa. We can sketch an outline of a proof;
+performing induction on ``n``, we have:
+
+-  Property ``prop`` is ``\x => plus x m = plus m x``.
+
+-  Show that ``prop`` holds in the base case and inductive step:
+
+   -  | Base case: ``prop Z``, i.e.
+      | ``plus Z m = plus m Z``, which reduces to
+      | ``m = plus m Z`` due to the definition of ``plus``.
+
+   -  | Inductive step: Inductively, we know that ``prop k`` holds for a specific, fixed ``k``, i.e.
+      | ``plus k m = plus m k`` (the induction hypothesis). Given this, show ``prop (S k)``, i.e.
+      | ``plus (S k) m = plus m (S k)``, which reduces to
+      | ``S (plus k m) = plus m (S k)``. From the induction hypothesis, we can rewrite this to
+      | ``S (plus m k) = plus m (S k)``.
+
+To complete the proof we therefore need to show that ``m = plus m Z``
+for all natural numbers ``m``, and that ``S (plus m k) = plus m (S k)``
+for all natural numbers ``m`` and ``k``. Each of these can also be
+proved by induction, this time on ``m``.
+
+We are now ready to embark on a proof of commutativity of ``plus``
+formally in Idris.

docs/source/proofs/patterns.rst

@@ -0,0 +1,320 @@
+***********************
+Pattern Matching Proofs
+***********************
+
+In this section, we will provide a proof of ``plus_commutes`` directly,
+by writing a pattern matching definition. We will use interactive
+editing features extensively, since it is significantly easier to
+produce a proof when the machine can give the types of intermediate
+values and construct components of the proof itself. The commands we
+will use are summarised below. Where we refer to commands
+directly, we will use the Vim version, but these commands have a direct
+mapping to Emacs commands.
+
++---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
+|Command              | Vim binding     | Emacs binding | Explanation                                                                                |
++---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
+| Check type          | ``\t``          | ``C-c C-t``   | Show type of identifier or hole under the cursor.                                          |
++---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
+| Proof search        | ``\s``          | ``C-c C-a``   | Attempt to solve hole under the cursor by applying simple proof search.                    |
++---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
+| Make new definition | ``\a``          | ``C-c C-s``   | Add a template definition for the type defined under the cursor.                           |
++---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
+| Make lemma          | ``\l``          | ``C-c C-e``   | Add a top level function with a type which solves the hole under the cursor.               |
++---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
+| Split cases         | ``\c``          | ``C-c C-c``   | Create new constructor patterns for each possible case of the variable under the cursor.   |
++---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
+
+
+Creating a Definition
+=====================
+
+To begin, create a file ``pluscomm.idr`` containing the following type
+declaration:
+
+.. code-block:: idris
+
+    plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
+
+To create a template definition for the proof, press ``\a`` (or the
+equivalent in your editor of choice) on the line with the type
+declaration. You should see:
+
+.. code-block:: idris
+
+    plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
+    plus_commutes n m = ?plus_commutes_rhs
+
+To prove this by induction on ``n``, as we sketched in Section
+:ref:`sect-inductive`, we begin with a case split on ``n`` (press
+``\c`` with the cursor over the ``n`` in the definition.) You
+should see:
+
+.. code-block:: idris
+
+    plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
+    plus_commutes Z m = ?plus_commutes_rhs_1
+    plus_commutes (S k) m = ?plus_commutes_rhs_2
+
+If we inspect the types of the newly created holes,
+``plus_commutes_rhs_1`` and ``plus_commutes_rhs_2``, we see that the
+type of each reflects that ``n`` has been refined to ``Z`` and ``S k``
+in each respective case. Pressing ``\t`` over
+``plus_commutes_rhs_1`` shows:
+
+.. code-block:: idris
+
+       m : Nat
+    -------------------------------------
+    plus_commutes_rhs_1 : m = plus m Z
+
+Similarly, for ``plus_commutes_rhs_2``:
+
+.. code-block:: idris
+
+      k : Nat
+      m : Nat
+    --------------------------------------
+    plus_commutes_rhs_2 : (S (plus k m)) = (plus m (S k))
+
+It is a good idea to give these slightly more meaningful names:
+
+.. code-block:: idris
+
+    plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
+    plus_commutes Z m = ?plus_commutes_Z
+    plus_commutes (S k) m = ?plus_commutes_S
+
+Base Case
+=========
+
+We can create a separate lemma for the base case interactively, by
+pressing ``\l`` with the cursor over ``plus_commutes_Z``. This
+yields:
+
+.. code-block:: idris
+
+    plus_commutes_Z : (m : Nat) -> m = plus m Z
+
+    plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
+    plus_commutes Z m = plus_commutes_Z m
+    plus_commutes (S k) m = ?plus_commutes_S
+
+That is, the hole has been filled with a call to a top level
+function ``plus_commutes_Z``, applied to the variable in scope ``m``. 
+
+Unfortunately, we cannot prove this lemma directly, since ``plus`` is
+defined by matching on its *first* argument, and here ``plus m Z`` has a
+concrete value for its *second argument* (in fact, the left hand side of
+the equality has been reduced from ``plus Z m``.) Again, we can prove
+this by induction, this time on ``m``.
+
+First, create a template definition with ``\d``:
+
+.. code-block:: idris
+
+    plus_commutes_Z : (m : Nat) -> m = plus m Z 
+    plus_commutes_Z m = ?plus_commutes_Z_rhs
+
+Now, case split on ``m`` with ``\c``:
+
+.. code-block:: idris
+
+    plus_commutes_Z : (m : Nat) -> m = plus m Z 
+    plus_commutes_Z Z = ?plus_commutes_Z_rhs_1
+    plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2
+
+Checking the type of ``plus_commutes_Z_rhs_1`` shows the following,
+which is provable by ``Refl``:
+
+.. code-block:: idris
+
+    --------------------------------------
+    plus_commutes_Z_rhs_1 : Z = Z
+
+For such immediate proofs, we can let write the proof automatically by
+pressing ``\s`` with the cursor over ``plus_commutes_Z_rhs_1``.
+This yields:
+
+.. code-block:: idris
+
+    plus_commutes_Z : (m : Nat) -> m = plus m Z
+    plus_commutes_Z Z = Refl
+    plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2
+
+For ``plus_commutes_Z_rhs_2``, we are not so lucky:
+
+.. code-block:: idris
+
+       k : Nat
+    -------------------------------------
+    plus_commutes_Z_rhs_2 : S k = S (plus k Z)
+
+Inductively, we should know that ``k = plus k Z``, and we can get access
+to this inductive hypothesis by making a recursive call on k, as
+follows:
+
+.. code-block:: idris
+
+    plus_commutes_Z : (m : Nat) -> m = plus m Z
+    plus_commutes_Z Z = Refl
+    plus_commutes_Z (S k)
+       = let rec = plus_commutes_Z k in
+             ?plus_commutes_Z_rhs_2
+
+For ``plus_commutes_Z_rhs_2``, we now see:
+
+.. code-block:: idris
+
+       k : Nat
+       rec : k = plus k Z
+    -------------------------------------
+    plus_commutes_Z_rhs_2 : S k = S (plus k Z)
+
+So we know that ``k = plus k Z``, but how do we use this to update the goal to
+``S k = S k``?
+
+To achieve this, Idris provides a ``replace`` function as part of the
+prelude:
+
+.. code-block:: idris
+
+    Main> :t replace
+    Builtin.replace : (0 rule : x = y) -> p x -> p y
+
+Given a proof that ``x = y``, and a property ``p`` which holds for
+``x``, we can get a proof of the same property for ``y``, because we
+know ``x`` and ``y`` must be the same. Note the multiplicity on ``rule``
+means that it's guaranteed to be erased at run time.
+In practice, this function can be
+a little tricky to use because in general the implicit argument ``p``
+can be hard to infer by unification, so Idris provides a high level
+syntax which calculates the property and applies ``replace``:
+
+.. code-block:: idris
+
+    rewrite prf in expr
+
+If we have ``prf : x = y``, and the required type for ``expr`` is some
+property of ``x``, the ``rewrite ... in`` syntax will search for all
+occurrences of ``x``
+in the required type of ``expr`` and replace them with ``y``. We want
+to replace ``plus k Z`` with ``k``, so we need to apply our rule
+``rec`` in reverse, which we can do using ``sym`` from the Prelude
+
+.. code-block:: idris
+
+    Main> :t sym
+    Builtin.sym : (0 rule : x = y) -> y = x
+
+Concretely, in our example, we can say:
+
+.. code-block:: idris
+
+    plus_commutes_Z (S k)
+       = let rec = plus_commutes_Z k in
+             rewrite sym rec in ?plus_commutes_Z_rhs_2
+
+Checking the type of ``plus_commutes_Z_rhs_2`` now gives:
+
+.. code-block:: idris
+
+       k : Nat
+       rec : k = plus k Z
+    -------------------------------------
+    plus_commutes_Z_rhs_2 : S k = S k
+
+Using the rewrite rule ``rec``, the goal type has been updated with ``plus k Z``
+replaced by ``k``.
+
+We can use proof search (``\s``) to complete the proof, giving:
+
+.. code-block:: idris
+
+    plus_commutes_Z : (m : Nat) -> m = plus m Z
+    plus_commutes_Z Z = Refl
+    plus_commutes_Z (S k)
+       = let rec = plus_commutes_Z k in
+             rewrite sym rec in Refl
+
+The base case of ``plus_commutes`` is now complete.
+
+Inductive Step
+==============
+
+Our main theorem, ``plus_commutes`` should currently be in the following
+state:
+
+.. code-block:: idris
+
+    plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
+    plus_commutes Z m = plus_commutes_Z m
+    plus_commutes (S k) m = ?plus_commutes_S
+
+Looking again at the type of ``plus_commutes_S``, we have:
+
+.. code-block:: idris
+
+       k : Nat
+       m : Nat
+    -------------------------------------
+    plus_commutes_S : S (plus k m) = plus m (S k)
+
+Conveniently, by induction we can immediately tell that
+``plus k m = plus m k``, so let us rewrite directly by making a
+recursive call to ``plus_commutes``. We add this directly, by hand, as
+follows:
+
+.. code-block:: idris
+
+    plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
+    plus_commutes Z m = plus_commutes_Z
+    plus_commutes (S k) m = rewrite plus_commutes k m in ?plus_commutes_S
+
+Checking the type of ``plus_commutes_S`` now gives:
+
+.. code-block:: idris
+
+       k : Nat
+       m : Nat
+    -------------------------------------
+    plus_commutes_S : S (plus m k) = plus m (S k)
+
+The good news is that ``m`` and ``k`` now appear in the correct order.
+However, we still have to show that the successor symbol ``S`` can be
+moved to the front in the right hand side of this equality. This
+remaining lemma takes a similar form to the ``plus_commutes_Z``; we
+begin by making a new top level lemma with ``\l``. This gives:
+
+.. code-block:: idris
+
+    plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
+
+Again, we make a template definition with ``\a``:
+
+.. code-block:: idris
+
+    plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
+    plus_commutes_S k m = ?plus_commutes_S_rhs
+
+Like ``plus_commutes_Z``, we can define this by induction over ``m``, since
+``plus`` is defined by matching on its first argument. The complete definition
+is:
+
+.. code-block:: idris
+
+    total
+    plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
+    plus_commutes_S k Z = Refl
+    plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
+
+All holes have now been solved.
+
+The ``total`` annotation means that we require the final function to
+pass the totality checker; i.e. it will terminate on all possible
+well-typed inputs. This is important for proofs, since it provides a
+guarantee that the proof is valid in *all* cases, not just those for
+which it happens to be well-defined.
+
+Now that ``plus_commutes`` has a ``total`` annotation, we have completed the
+proof of commutativity of addition on natural numbers.

docs/source/proofs/pluscomm.rst

@@ -0,0 +1,185 @@
+********************************************
+Running example: Addition of Natural Numbers
+********************************************
+
+Throughout this tutorial, we will be working with the following
+function, defined in the Idris prelude, which defines addition on
+natural numbers:
+
+.. code-block:: idris
+
+    plus : Nat -> Nat -> Nat
+    plus Z     m = m
+    plus (S k) m = S (plus k m)
+
+It is defined by the above equations, meaning that we have for free the
+properties that adding ``m`` to zero always results in ``m``, and that
+adding ``m`` to any non-zero number ``S k`` always results in
+``S (plus k m)``. We can see this by evaluation at the Idris REPL (i.e.
+the prompt, the read-eval-print loop):
+
+.. code-block:: idris
+
+    Main> \m => plus Z m
+    \m => m
+
+    Idris> \k,m => plus (S k) m
+    \k => \m => S (plus k m)
+
+Note that unlike many other language REPLs, the Idris REPL performs
+evaluation on *open* terms, meaning that it can reduce terms which
+appear inside lambda bindings, like those above. Therefore, we can
+introduce unknowns ``k`` and ``m`` as lambda bindings and see how
+``plus`` reduces.
+
+The ``plus`` function has a number of other useful properties, for
+example:
+
+-  It is *commutative*, that is for all ``Nat`` inputs ``n`` and ``m``,
+   we know that ``plus n m = plus m n``.
+
+-  It is *associative*, that is for all ``Nat`` inputs ``n``, ``m`` and
+   ``p``, we know that ``plus n (plus m p) = plus (plus m n) p``.
+
+We can use these properties in an Idris program, but in order to do so
+we must *prove* them.
+
+Equality Proofs
+===============
+
+Idris defines a propositional equality type as follows:
+
+.. code-block:: idris
+
+    data Equal : a -> b -> Type where
+       Refl : Equal x x
+
+As syntactic sugar, ``Equal x y`` can be written as ``x = y``.
+
+It is *propositional* equality, where the type states that any two
+values in different types ``a`` and ``b`` may be proposed to be equal.
+There is only one way to *prove* equality, however, which is by
+reflexivity (``Refl``).
+
+We have a *type* for propositional equality here, and correspondingly a
+*program* inhabiting an instance of this type can be seen as a proof of
+the corresponding proposition [1]_. So, trivially, we can prove that
+``4`` equals ``4``:
+
+.. code-block:: idris
+
+    four_eq : 4 = 4
+    four_eq = Refl
+
+However, trying to prove that ``4 = 5`` results in failure:
+
+.. code-block:: idris
+
+    four_eq_five : 4 = 5
+    four_eq_five = Refl
+
+The type ``4 = 5`` is a perfectly valid type, but is uninhabited, so
+when trying to type check this definition, Idris gives the following
+error:
+
+::
+
+    When unifying 4 = 4 and (fromInteger 4) = (fromInteger 5)
+    Mismatch between:
+            4
+    and
+            5
+
+Type checking equality proofs
+-----------------------------
+
+An important step in type checking Idris programs is *unification*,
+which attempts to resolve implicit arguments such as the implicit
+argument ``x`` in ``Refl``. As far as our understanding of type checking
+proofs is concerned, it suffices to know that unifying two terms
+involves reducing both to normal form then trying to find an assignment
+to implicit arguments which will make those normal forms equal.
+
+When type checking ``Refl``, Idris requires that the type is of the form
+``x = x``, as we see from the type of ``Refl``. In the case of
+``four_eq_five``, Idris will try to unify the expected type ``4 = 5``
+with the type of ``Refl``, ``x = x``, notice that a solution requires
+that ``x`` be both ``4`` and ``5``, and therefore fail.
+
+Since type checking involves reduction to normal form, we can write the
+following equalities directly:
+
+.. code-block:: idris
+
+    twoplustwo_eq_four : 2 + 2 = 4
+    twoplustwo_eq_four = Refl
+
+    plus_reduces_Z : (m : Nat) -> plus Z m = m
+    plus_reduces_Z m = Refl
+
+    plus_reduces_Sk : (k, m : Nat) -> plus (S k) m = S (plus k m)
+    plus_reduces_Sk k m = Refl
+
+Heterogeneous Equality
+======================
+
+Equality in Idris is *heterogeneous*, meaning that we can even propose
+equalities between values in different types:
+
+.. code-block:: idris
+
+    idris_not_php : Z = "Z"
+
+The type ``Z = "Z"`` is uninhabited, and one might wonder why it is useful to
+be able to propose equalities between values in different types. However, with
+dependent types, such equalities can arise naturally. For example, if two
+vectors are equal, their lengths must be equal:
+
+.. code-block:: idris
+
+    vect_eq_length : (xs : Vect n a) -> (ys : Vect m a) ->
+                     (xs = ys) -> n = m
+
+In the above declaration, ``xs`` and ``ys`` have different types because
+their lengths are different, but we would still like to draw a
+conclusion about the lengths if they happen to be equal. We can define
+``vect_eq_length`` as follows:
+
+.. code-block:: idris
+
+    vect_eq_length xs xs Refl = Refl
+
+By matching on ``Refl`` for the third argument, we know that the only
+valid value for ``ys`` is ``xs``, because they must be equal, and
+therefore their types must be equal, so the lengths must be equal.
+
+Alternatively, we can put an underscore for the second ``xs``, since
+there is only one value which will type check:
+
+.. code-block:: idris
+
+    vect_eq_length xs _ Refl = Refl
+
+Properties of ``plus``
+======================
+
+Using the ``(=)`` type, we can now state the properties of ``plus``
+given above as Idris type declarations:
+
+.. code-block:: idris
+
+    plus_commutes : (n, m : Nat) -> plus n m = plus m n
+    plus_assoc : (n, m, p : Nat) -> plus n (plus m p) = plus (plus n m) p
+
+Both of these properties (and many others) are proved for natural number
+addition in the Idris standard library, using ``(+)`` from the ``Num``
+interface rather than using ``plus`` directly. They have the names
+``plusCommutative`` and ``plusAssociative`` respectively.
+
+In the remainder of this tutorial, we will explore several different
+ways of proving ``plus_commutes`` (or, to put it another way, writing
+the function.) We will also discuss how to use such equality proofs, and
+see where the need for them arises in practice.
+
+.. [1]
+   This is known as the Curry-Howard correspondence.

docs/source/proofs/propositional.rst

@@ -0,0 +1,135 @@
+This page attempts to explain some of the techniques used in Idris to prove
+propositional equalities.
+
+Proving Propositional Equality
+==============================
+
+We have seen that definitional equalities can be proved using ``Refl`` since they
+always normalise to values that can be compared directly.
+
+However with propositional equalities we are using symbolic variables, which do
+not always normalse.
+
+So to take the previous example:
+
+.. code-block:: idris
+
+    plusReducesR : (n : Nat) -> plus n Z = n
+
+In this case ``plus n Z`` does not normalise to n. Even though both sides of
+the equality are provably equal we cannot claim ``Refl`` as a proof.
+
+If the pattern match cannot match for all ``n`` then we need to
+match all possible values of ``n``. In this case
+
+.. code-block:: idris
+
+   plusReducesR : (n : Nat) -> plus n Z = n
+   plusReducesR Z = Refl
+   plusReducesR (S k) 
+       = let rec = plusReducesR k in
+             rewrite sym rec in Refl
+
+we can't use ``Refl`` to prove ``n = plus n 0`` for all ``n``. Instead, we call
+it for each case separately.  So, in the second line for example, the type checker
+substitutes ``Z`` for ``n`` in the type being matched, and reduces the type
+accordingly.
+
+Replace
+=======
+
+This implements the 'indiscernability of identicals' principle, if two terms
+are equal then they have the same properties. In other words, if ``x=y``, then we
+can substitute y for x in any expression. In our proofs we can express this as:
+
+   if x=y
+   then prop x = prop y
+
+where prop is a pure function representing the property. In the examples below
+prop is an expression in some variable with a type like this: ``prop: n -> Type``
+
+So if ``n`` is a natural number variable then ``prop`` could be something
+like ``\n => 2*n + 3``.
+
+To use this in our proofs there is the following function in the prelude:
+
+.. code-block:: idris
+
+   ||| Perform substitution in a term according to some equality.
+   replace : forall x, y, prop . (0 rule : x = y) -> prop x -> prop y
+   replace Refl prf = prf
+
+If we supply an equality (x=y) and a proof of a property of x (``prop x``) then we get
+a proof of a property of y (``prop y``).
+So, in the following example, if we supply ``p1 x`` which is a proof that ``x=2`` and
+the equality ``x=y`` then we get a proof that ``y=2``.
+
+.. code-block:: idris
+
+   p1: Nat -> Type
+   p1 n = (n=2)
+
+   testReplace: (x=y) -> (p1 x) -> (p1 y)
+   testReplace a b = replace a b
+
+Rewrite
+=======
+
+In practice, ``replace`` can be
+a little tricky to use because in general the implicit argument ``prop``
+can be hard to infer for the machine, so Idris provides a high level
+syntax which calculates the property and applies ``replace``.
+
+Example: again we supply ``p1`` which is a proof that ``x=2`` and the equality
+``x=y`` then we get a proof that ``y=2``.
+
+.. code-block:: idris
+
+   p1: Nat -> Type
+   p1 x = (x=2)
+
+   testRewrite2: (x=y) -> (p1 y) -> (p1 x)
+   testRewrite2 a b = rewrite a in b
+
+We can think of ``rewrite`` as working in this way:
+
+ * Start with a equation ``x=y`` and a property ``prop : x -> Type``
+ * Search for ``x`` in ``prop``
+ * Replaces all occurrences of ``x`` with ``y`` in ``prop``.
+
+That is, we are doing a substitution.
+
+Symmetry and Transitivity
+=========================
+
+In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity'
+and these are also included in the prelude:
+
+.. code-block:: idris
+
+   ||| Symmetry of propositional equality
+   sym : forall x, y . (0 rule : x = y) -> y = x
+   sym Refl = Refl
+
+   ||| Transitivity of propositional equality
+   trans : forall a, b, c . (0 l : a = b) -> (0 r : b = c) -> a = c
+   trans Refl Refl = Refl
+
+Heterogeneous Equality
+======================
+
+Also included in the prelude: 
+
+.. code-block:: idris
+
+   ||| Explicit heterogeneous ("John Major") equality. Use this when Idris
+   ||| incorrectly chooses homogeneous equality for `(=)`.
+   ||| @ a the type of the left side
+   ||| @ b the type of the right side
+   ||| @ x the left side
+   ||| @ y the right side
+   (~=~) : (x : a) -> (y : b) -> Type
+   (~=~) x y = (x = y)
+
+
+

docs/source/reference/envvars.rst

@@ -0,0 +1,7 @@
+.. _ref-sect-envvars:
+
+*********************
+Environment Variables
+*********************
+
+[TODO: Fill in the environment variables recognised by Idris 2]

docs/source/reference/index.rst

@@ -0,0 +1,20 @@
+**********************
+Idris2 Reference Guide
+**********************
+
+.. note::
+
+   The documentation for Idris 2 has been published under the Creative
+   Commons CC0 License. As such to the extent possible under law, *The
+   Idris Community* has waived all copyright and related or neighboring
+   rights to Documentation for Idris.
+
+   More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
+
+This is a placeholder, to get set up with readthedocs.
+
+.. toctree::
+   :maxdepth: 1
+
+   packages
+   envvars

docs/source/reference/packages.rst

@@ -0,0 +1,106 @@
+.. _ref-sect-packages:
+
+********
+Packages
+********
+
+Idris includes a simple system for building packages from a package
+description file.  These files can be used with the Idris compiler to
+manage the development process of your Idris programmes and packages.
+
+Package Descriptions
+====================
+
+A package description includes the following:
+
++ A header, consisting of the keyword package followed by the package
+  name. Package names can be any valid Idris identifier. The iPKG
+  format also takes a quoted version that accepts any valid filename.
++ Fields describing package contents, ``<field> = <value>``
+
+At least one field must be the modules field, where the value is a
+comma separated list of modules.  For example, a library test which
+has two modules ``Foo.idr`` and ``Bar.idr`` as source files would be
+written as follows::
+
+    package test
+
+    modules = Foo, Bar
+
+Other examples of package files can be found in the ``libs`` directory
+of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
+
+Metadata
+--------
+
+The `iPKG` format supports additional metadata associated with the package.
+The added fields are:
+
++ ``brief = "<text>"``, a string literal containing a brief description
+  of the package.
+
++ ``version = "<text>""``, a version string to associate with the package.
+
++ ``readme = "<file>""``, location of the README file.
+
++ ``license = "<text>"``, a string description of the licensing
+  information.
+
++ ``authors = "<text>"``, the author information.
+
++ ``maintainers = "<text>"``, Maintainer information.
+
++ ``homepage = "<url>"``, the website associated with the package.
+
++ ``sourceloc = "<url>"``, the location of the DVCS where the source
+  can be found.
+
++ ``bugtracker = "<url>"``, the location of the project's bug tracker.
+
+
+Common Fields
+-------------
+
+Other common fields which may be present in an ``ipkg`` file are:
+
++ ``executable = <output>``, which takes the name of the executable
+  file to generate. Executable names can be any valid Idris
+  identifier. the iPKG format also takes a quoted version that accepts
+  any valid filename.
+
+  Executables are placed in ``build/exec``, relative to the top level
+  source directory.
+
++ ``main = <module>``, which takes the name of the main module, and
+  must be present if the executable field is present.
+
++ ``opts = "<idris options>"``, which allows options to be passed to
+  Idris.
+
++ ``depends = <pkg name> (',' <pkg name>)+``, a comma separated list of
+  package names that the Idris package requires.
+
+
+Comments
+---------
+
+Package files support comments using the standard Idris singleline ``--`` and multiline ``{- -}`` format.
+
+Using Package files
+===================
+
+Given an Idris package file ``test.ipkg`` it can be used with the Idris compiler as follows:
+
++ ``idris2 --build test.ipkg`` will build all modules in the package
+
++ ``idris2 --install test.ipkg`` will install the package, making it
+  accessible by other Idris libraries and programs. Note that this doesn't
+  install any executables, just library modules.
+
++ ``idris2 --clean test.ipkg`` will clean the intermediate build files.
+
+Once the test package has been installed, the command line option
+``--package test`` makes it accessible (abbreviated to ``-p test``).
+For example::
+
+    idris -p test Main.idr

docs/source/tutorial/conclusions.rst

@@ -0,0 +1,59 @@
+.. _sect-concs:
+
+***************
+Further Reading
+***************
+
+Further information about Idris programming, and programming with
+dependent types in general, can be obtained from various sources:
+
+*  `Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_
+   by Edwin Brady, available from `Manning <https://www.manning.com>`_.
+
+*  The Idris web site (http://www.idris-lang.org/) and by asking
+   questions on the mailing list.
+
+*  The IRC channel ``#idris``, on
+   `webchat.freenode.net <https://webchat.freenode.net/>`__.
+
+*  The wiki (https://github.com/idris-lang/Idris-dev/wiki/) has further
+   user provided information, in particular:
+
+   * https://github.com/idris-lang/Idris-dev/wiki/Manual
+
+   * https://github.com/idris-lang/Idris-dev/wiki/Language-Features
+
+*  Examining the prelude and exploring the ``samples`` in the
+   distribution. The Idris 2 source can be found online at:
+   
+   * https://github.com/edwinb/Idris2.
+
+*  Existing projects on the ``Idris Hackers`` web space:
+   
+   * http://idris-hackers.github.io.
+
+*  Various papers (e.g. [#BradyHammond2012]_, [#Brady]_, and [#BradyHammond2010]_).  Although these mostly
+   describe older versions of Idris.
+
+.. [#BradyHammond2012] Edwin Brady and Kevin Hammond. 2012. Resource-Safe systems
+       programming with embedded domain specific languages. In
+       Proceedings of the 14th international conference on Practical
+       Aspects of Declarative Languages (PADL'12), Claudio Russo and
+       Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg,
+       242-257. DOI=10.1007/978-3-642-27694-1_18
+       http://dx.doi.org/10.1007/978-3-642-27694-1_18
+
+.. [#Brady] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full
+       dependent types. In Proceedings of the 5th ACM workshop on
+       Programming languages meets program verification (PLPV
+       '11). ACM, New York, NY, USA,
+       43-54. DOI=10.1145/1929529.1929536
+       http://doi.acm.org/10.1145/1929529.1929536
+
+.. [#BradyHammond2010] Edwin C. Brady and Kevin Hammond. 2010. Scrapping your
+       inefficient engine: using partial evaluation to improve
+       domain-specific language implementation. In Proceedings of the
+       15th ACM SIGPLAN international conference on Functional
+       programming (ICFP '10). ACM, New York, NY, USA,
+       297-308. DOI=10.1145/1863543.1863587
+       http://doi.acm.org/10.1145/1863543.1863587

docs/source/tutorial/index.rst

@@ -0,0 +1,40 @@
+.. _tutorial-index:
+
+#########################
+A Crash Course in Idris 2
+#########################
+
+This is a crash course in Idris 2 (sort of a tutorial, but rather less
+gentle I'm afraid!).
+It provides a brief introduction to programming in the Idris Language.
+It covers the core language features, assuming some experience with an
+existing functional programming language such as Haskell or OCaml.
+
+This has been revised and updated from the Idris 1 tutorial. For details of
+changes since Idris 1, see :ref:`updates-index`.
+
+.. note::
+   The documentation for Idris has been published under the Creative
+   Commons CC0 License. As such to the extent possible under law, *The
+   Idris Community* has waived all copyright and related or neighboring
+   rights to Documentation for Idris.
+
+   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+
+
+.. toctree::
+   :maxdepth: 1
+
+   introduction
+   starting
+   typesfuns
+   interfaces
+   modules
+   multiplicities
+   packages
+   interp
+   views
+   theorems
+   interactive
+   miscellany
+   conclusions

docs/source/tutorial/interactive.rst

@@ -0,0 +1,256 @@
+.. _sect-interactive:
+
+*******************
+Interactive Editing
+*******************
+
+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 embedded DSL
+development by allowing a programmer to describe the type system of an
+object language. However, precise types give us more than verification
+of programs — we can also use the type system to help write programs which
+are *correct by construction*, interactively.
+
+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
+hole, and even a basic proof search mechanism. In this
+section, we explain how these features can be exploited by a text
+editor, and specifically how to do so in `Vim
+<https://github.com/edwinb/idris2-vim>`_. An interactive mode
+for `Emacs <https://github.com/idris-hackers/idris-mode>`_ is also
+available (though not yet updated for Idris 2).
+
+Editing at the REPL
+===================
+
+The REPL provides a number of commands, which we will describe
+shortly, which generate new program fragments based on the currently
+loaded module. These take the general form:
+
+::
+
+    :command [line number] [name]
+
+That is, each command acts on a specific source line, at a specific
+name, and outputs a new program fragment. Each command has an
+alternative form, which *updates* the source file in-place:
+
+::
+
+    :command! [line number] [name]
+
+It is also possible to invoke Idris in a mode which runs a REPL command,
+displays the result, then exits, using ``idris2 --client``. For example:
+
+::
+
+    $ idris2 --client ':t plus'
+    Prelude.plus : Nat -> Nat -> Nat
+    $ idris2 --client '2+2'
+    4
+
+A text editor can take advantage of this, along with the editing
+commands, in order to provide interactive editing support.
+
+Editing Commands
+================
+
+:addclause
+----------
+
+The ``:addclause n f`` command, abbreviated ``:ac n f``, creates a
+template definition for the function named ``f`` declared on line
+``n``. For example, if the code beginning on line 94 contains:
+
+.. code-block:: idris
+
+    vzipWith : (a -> b -> c) ->
+               Vect n a -> Vect n b -> Vect n c
+
+then ``:ac 94 vzipWith`` will give:
+
+.. code-block:: idris
+
+    vzipWith f xs ys = ?vzipWith_rhs
+
+The names are chosen according to hints which may be given by a
+programmer, and then made unique by the machine by adding a digit if
+necessary. Hints can be given as follows:
+
+.. code-block:: idris
+
+    %name Vect xs, ys, zs, ws
+
+This declares that any names generated for types in the ``Vect`` family
+should be chosen in the order ``xs``, ``ys``, ``zs``, ``ws``.
+
+:casesplit
+----------
+
+The ``:casesplit n x`` command, abbreviated ``:cs n x``, splits the
+pattern variable ``x`` on line ``n`` into the various pattern forms it
+may take, removing any cases which are impossible due to unification
+errors. For example, if the code beginning on line 94 is:
+
+.. code-block:: idris
+
+    vzipWith : (a -> b -> c) ->
+               Vect n a -> Vect n b -> Vect n c
+    vzipWith f xs ys = ?vzipWith_rhs
+
+then ``:cs 96 xs`` will give:
+
+.. code-block:: idris
+
+    vzipWith f [] ys = ?vzipWith_rhs_1
+    vzipWith f (x :: xs) ys = ?vzipWith_rhs_2
+
+That is, the pattern variable ``xs`` has been split into the two
+possible cases ``[]`` and ``x :: xs``. Again, the names are chosen
+according to the same heuristic. If we update the file (using
+``:cs!``) then case split on ``ys`` on the same line, we get:
+
+.. code-block:: idris
+
+    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 ::
+ys`` would lead to a unification error.
+
+:addmissing
+-----------
+
+The ``:addmissing n f`` command, abbreviated ``:am n f``, adds the
+clauses which are required to make the function ``f`` on line ``n``
+cover all inputs. For example, if the code beginning on line 94 is:
+
+.. code-block:: idris
+
+    vzipWith : (a -> b -> c) ->
+               Vect n a -> Vect n b -> Vect n c
+    vzipWith f [] [] = ?vzipWith_rhs_1
+
+then ``:am 96 vzipWith`` gives:
+
+.. code-block:: idris
+
+    vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2
+
+That is, it notices that there are no cases for empty vectors,
+generates the required clauses, and eliminates the clauses which would
+lead to unification errors.
+
+:proofsearch
+------------
+
+The ``:proofsearch n f`` command, abbreviated ``:ps n f``, attempts to
+find a value for the hole ``f`` on line ``n`` by proof search,
+trying values of local variables, recursive calls and constructors of
+the required family. Optionally, it can take a list of *hints*, which
+are functions it can try applying to solve the hole. For
+example, if the code beginning on line 94 is:
+
+.. code-block:: idris
+
+    vzipWith : (a -> b -> c) ->
+               Vect n a -> Vect n b -> Vect n c
+    vzipWith f [] [] = ?vzipWith_rhs_1
+    vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2
+
+then ``:ps 96 vzipWith_rhs_1`` will give
+
+.. code-block:: idris
+
+   []
+
+This works because it is searching for a ``Vect`` of length 0, of
+which the empty vector is the only possibility. Similarly, and perhaps
+surprisingly, there is only one possibility if we try to solve ``:ps
+97 vzipWith_rhs_2``:
+
+.. code-block:: idris
+
+    f x y :: vzipWith f xs ys
+
+This works because ``vzipWith`` has a precise enough type: The
+resulting vector has to be non-empty (a ``::``); the first element
+must have type ``c`` and the only way to get this is to apply ``f`` to
+``x`` and ``y``; finally, the tail of the vector can only be built
+recursively.
+
+:makewith
+---------
+
+The ``:makewith n f`` command, abbreviated ``:mw n f``, adds a
+``with`` to a pattern clause. For example, recall ``parity``. If line
+10 is:
+
+.. code-block:: idris
+
+    parity (S k) = ?parity_rhs
+
+then ``:mw 10 parity`` will give:
+
+.. code-block:: idris
+
+    parity (S k) with (_)
+      parity (S k) | with_pat = ?parity_rhs
+
+If we then fill in the placeholder ``_`` with ``parity k`` and case
+split on ``with_pat`` using ``:cs 11 with_pat`` we get the following
+patterns:
+
+.. code-block:: idris
+
+      parity (S (plus n n)) | even = ?parity_rhs_1
+      parity (S (S (plus n n))) | odd = ?parity_rhs_2
+
+Note that case splitting has normalised the patterns here (giving
+``plus`` rather than ``+``). In any case, we see that using
+interactive editing significantly simplifies the implementation of
+dependent pattern matching by showing a programmer exactly what the
+valid patterns are.
+
+Interactive Editing in Vim
+==========================
+
+The editor mode for Vim provides syntax highlighting, indentation and
+interactive editing support using the commands described above.
+Interactive editing is achieved using the following editor commands,
+each of which update the buffer directly:
+
+- ``\a`` adds a template definition for the name declared on the
+   current line (using ``:addclause``).
+
+- ``\c`` case splits the variable at the cursor (using
+   ``:casesplit``).
+
+- ``\m`` adds the missing cases for the name at the cursor (using
+   ``:addmissing``).
+
+- ``\w`` adds a ``with`` clause (using ``:makewith``).
+
+- ``\s`` invokes a proof search to solve the hole under the
+   cursor (using ``:proofsearch``).
+
+There are also commands to invoke the type checker and evaluator:
+
+- ``\t`` displays the type of the (globally visible) name under the
+   cursor. In the case of a hole, this displays the context
+   and the expected type.
+
+- ``\e`` prompts for an expression to evaluate.
+
+- ``\r`` reloads and type checks the buffer.
+
+Corresponding commands are also available in the Emacs mode. Support
+for other editors can be added in a relatively straightforward manner
+by using ``idris2 -–client``.
+More sophisticated support can be added by using the IDE protocol (yet to
+be documented for Idris 2, but which mostly extends to protocol documented for 
+`Idris 1 <http://docs.idris-lang.org/en/latest/reference/ide-protocol.html>`_.
+

docs/source/tutorial/interfaces.rst

@@ -0,0 +1,659 @@
+.. _sect-interfaces:
+
+**********
+Interfaces
+**********
+
+We often want to define functions which work across several different
+data types. For example, we would like arithmetic operators to work on
+``Int``, ``Integer`` and ``Double`` at the very least. We would like
+``==`` to work on the majority of data types. We would like to be able
+to display different types in a uniform way.
+
+To achieve this, we use *interfaces*, which are similar to type classes in
+Haskell or traits in Rust. To define an interface, we provide a collection of
+overloadable functions. A simple example is the ``Show``
+interface, which is defined in the prelude and provides an interface for
+converting values to ``String``:
+
+.. code-block:: idris
+
+    interface Show a where
+        show : a -> String
+
+This generates a function of the following type (which we call a
+*method* of the ``Show`` interface):
+
+.. code-block:: idris
+
+    show : Show a => a -> String
+
+We can read this as: “under the constraint that ``a`` has an implementation
+of ``Show``, take an input ``a`` and return a ``String``.” An implementation
+of an interface is defined by giving definitions of the methods of the interface.
+For example, the ``Show`` implementation for ``Nat`` could be defined as:
+
+.. code-block:: idris
+
+    Show Nat where
+        show Z = "Z"
+        show (S k) = "s" ++ show k
+
+::
+
+    Main> show (S (S (S Z)))
+    "sssZ" : String
+
+Only one implementation of an interface can be given for a type — implementations may
+not overlap. Implementation declarations can themselves have constraints.
+To help with resolution, the arguments of an implementation must be
+constructors (either data or type constructors) or variables
+(i.e. you cannot give an implementation for a function). For
+example, to define a ``Show`` implementation for vectors, we need to know
+that there is a ``Show`` implementation for the element type, because we are
+going to use it to convert each element to a ``String``:
+
+.. code-block:: idris
+
+    Show a => Show (Vect n a) where
+        show xs = "[" ++ show' xs ++ "]" where
+            show' : forall n . Vect n a -> String
+            show' Nil        = ""
+            show' (x :: Nil) = show x
+            show' (x :: xs)  = show x ++ ", " ++ show' xs
+
+Note that we need the explicit ``forall n .`` in the ``show'`` function
+because otherwise the ``n`` is already in scope, and fixed to the value of
+the top level ``n``.
+
+Default Definitions
+===================
+
+The Prelude defines an ``Eq`` interface which provides methods for
+comparing values for equality or inequality, with implementations for all of
+the built-in types:
+
+.. code-block:: idris
+
+    interface Eq a where
+        (==) : a -> a -> Bool
+        (/=) : a -> a -> Bool
+
+To declare an implementation for a type, we have to give definitions of all
+of the methods. For example, for an implementation of ``Eq`` for ``Nat``:
+
+.. code-block:: idris
+
+    Eq Nat where
+        Z     == Z     = True
+        (S x) == (S y) = x == y
+        Z     == (S y) = False
+        (S x) == Z     = False
+
+        x /= y = not (x == y)
+
+It is hard to imagine many cases where the ``/=`` method will be
+anything other than the negation of the result of applying the ``==``
+method. It is therefore convenient to give a default definition for
+each method in the interface declaration, in terms of the other method:
+
+.. code-block:: idris
+
+    interface Eq a where
+        (==) : a -> a -> Bool
+        (/=) : a -> a -> Bool
+
+        x /= y = not (x == y)
+        x == y = not (x /= y)
+
+A minimal complete implementation of ``Eq`` requires either
+``==`` or ``/=`` to be defined, but does not require both. If a method
+definition is missing, and there is a default definition for it, then
+the default is used instead.
+
+Extending Interfaces
+====================
+
+Interfaces can also be extended. A logical next step from an equality
+relation ``Eq`` is to define an ordering relation ``Ord``. We can
+define an ``Ord`` interface which inherits methods from ``Eq`` as well as
+defining some of its own:
+
+.. code-block:: idris
+
+    data Ordering = LT | EQ | GT
+
+.. code-block:: idris
+
+    interface Eq a => Ord a where
+        compare : a -> a -> Ordering
+
+        (<) : a -> a -> Bool
+        (>) : a -> a -> Bool
+        (<=) : a -> a -> Bool
+        (>=) : a -> a -> Bool
+        max : a -> a -> a
+        min : a -> a -> a
+
+The ``Ord`` interface allows us to compare two values and determine their
+ordering. Only the ``compare`` method is required; every other method
+has a default definition. Using this we can write functions such as
+``sort``, a function which sorts a list into increasing order,
+provided that the element type of the list is in the ``Ord`` interface. We
+give the constraints on the type variables left of the fat arrow
+``=>``, and the function type to the right of the fat arrow:
+
+.. code-block:: idris
+
+    sort : Ord a => List a -> List a
+
+Functions, interfaces and implementations can have multiple
+constraints. Multiple constraints are written in brackets in a comma
+separated list, for example:
+
+.. code-block:: idris
+
+    sortAndShow : (Ord a, Show a) => List a -> String
+    sortAndShow xs = show (sort xs)
+
+Constraints are, like types, first class objects in the language. You can
+see this at the REPL:
+
+::
+
+    Main> :t Ord
+    Prelude.Ord : Type -> Type
+
+So, ``(Ord a, Show a)`` is an ordinary pair of ``Types``, with two constraints
+as the first and second element of the pair.
+
+Note: Interfaces and ``mutual`` blocks
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Idris is strictly "define before use", except in ``mutual`` blocks.
+In a ``mutual`` block, Idris elaborates in two passes: types on the first
+pass and definitions on the second. When the mutual block contains an
+interface declaration, it elaborates the interface header but none of the
+method types on the first pass, and elaborates the method types and any
+default definitions on the second pass.
+
+Functors and Applicatives
+=========================
+
+So far, we have seen single parameter interfaces, where the parameter
+is of type ``Type``. In general, there can be any number of parameters
+(even zero), and the parameters can have *any* type. If the type
+of the parameter is not ``Type``, we need to give an explicit type
+declaration. For example, the ``Functor`` interface is defined in the
+prelude:
+
+.. code-block:: idris
+
+    interface Functor (f : Type -> Type) where
+        map : (m : a -> b) -> f a -> f b
+
+A functor allows a function to be applied across a structure, for
+example to apply a function to every element in a ``List``:
+
+.. code-block:: idris
+
+    Functor List where
+      map f []      = []
+      map f (x::xs) = f x :: map f xs
+
+::
+
+    Idris> map (*2) [1..10]
+    [2, 4, 6, 8, 10, 12, 14, 16, 18, 20] : List Integer
+
+Having defined ``Functor``, we can define ``Applicative`` which
+abstracts the notion of function application:
+
+.. code-block:: idris
+
+    infixl 2 <*>
+
+    interface Functor f => Applicative (f : Type -> Type) where
+        pure  : a -> f a
+        (<*>) : f (a -> b) -> f a -> f b
+
+.. _monadsdo:
+
+Monads and ``do``-notation
+==========================
+
+The ``Monad`` interface allows us to encapsulate binding and computation,
+and is the basis of ``do``-notation introduced in Section
+:ref:`sect-do`. It extends ``Applicative`` as defined above, and is
+defined as follows:
+
+.. code-block:: idris
+
+    interface Applicative m => Monad (m : Type -> Type) where
+        (>>=)  : m a -> (a -> m b) -> m b
+
+Inside a ``do`` block, the following syntactic transformations are
+applied:
+
+- ``x <- v; e`` becomes ``v >>= (\x => e)``
+
+- ``v; e`` becomes ``v >>= (\_ => e)``
+
+- ``let x = v; e`` becomes ``let x = v in e``
+
+``IO`` has an implementation of ``Monad``, defined using primitive functions.
+We can also define an implementation for ``Maybe``, as follows:
+
+.. code-block:: idris
+
+    Monad Maybe where
+        Nothing  >>= k = Nothing
+        (Just x) >>= k = k x
+
+Using this we can, for example, define a function which adds two
+``Maybe Int``, using the monad to encapsulate the error handling:
+
+.. code-block:: idris
+
+    m_add : Maybe Int -> Maybe Int -> Maybe Int
+    m_add x y = do x' <- x -- Extract value from x
+                   y' <- y -- Extract value from y
+                   pure (x' + y') -- Add them
+
+This function will extract the values from ``x`` and ``y``, if they
+are both available, or return ``Nothing`` if one or both are not ("fail fast"). Managing the
+``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the
+``do`` notation.
+
+::
+
+    Main> m_add (Just 82) (Just 22)
+    Just 94
+    Main> m_add (Just 82) Nothing
+    Nothing
+
+Pattern Matching Bind
+~~~~~~~~~~~~~~~~~~~~~
+
+Sometimes we want to pattern match immediately on the result of a function
+in ``do`` notation. For example, let's say we have a function ``readNumber``
+which reads a number from the console, returning a value of the form
+``Just x`` if the number is valid, or ``Nothing`` otherwise:
+
+.. code-block:: idris
+
+    readNumber : IO (Maybe Nat)
+    readNumber = do
+      input <- getLine
+      if all isDigit (unpack input)
+         then pure (Just (cast input))
+         else pure Nothing
+
+If we then use it to write a function to read two numbers, returning
+``Nothing`` if neither are valid, then we would like to pattern match
+on the result of ``readNumber``:
+
+.. code-block:: idris
+
+    readNumbers : IO (Maybe (Nat, Nat))
+    readNumbers =
+      do x <- readNumber
+         case x of
+              Nothing => pure Nothing
+              Just x_ok => do y <- readNumber
+                              case y of
+                                   Nothing => pure Nothing
+                                   Just y_ok => pure (Just (x_ok, y_ok))
+
+If there's a lot of error handling, this could get deeply nested very quickly!
+So instead, we can combine the bind and the pattern match in one line. For example,
+we could try pattern matching on values of the form ``Just x_ok``:
+
+.. code-block:: idris
+
+    readNumbers : IO (Maybe (Nat, Nat))
+    readNumbers
+      = do Just x_ok <- readNumber
+           Just y_ok <- readNumber
+           pure (Just (x_ok, y_ok))
+
+There is still a problem, however, because we've now omitted the case for
+``Nothing`` so ``readNumbers`` is no longer total! We can add the ``Nothing``
+case back as follows:
+
+.. code-block:: idris
+
+    readNumbers : IO (Maybe (Nat, Nat))
+    readNumbers
+      = do Just x_ok <- readNumber 
+                | Nothing => pure Nothing
+           Just y_ok <- readNumber 
+                | Nothing => pure Nothing
+           pure (Just (x_ok, y_ok))
+
+The effect of this version of ``readNumbers`` is identical to the first (in
+fact, it is syntactic sugar for it and directly translated back into that form).
+The first part of each statement (``Just x_ok <-`` and ``Just y_ok <-``) gives
+the preferred binding - if this matches, execution will continue with the rest
+of the ``do`` block. The second part gives the alternative bindings, of which
+there may be more than one.
+
+``!``-notation
+~~~~~~~~~~~~~~
+
+In many cases, using ``do``-notation can make programs unnecessarily
+verbose, particularly in cases such as ``m_add`` above where the value
+bound is used once, immediately. In these cases, we can use a
+shorthand version, as follows:
+
+.. code-block:: idris
+
+    m_add : Maybe Int -> Maybe Int -> Maybe Int
+    m_add x y = pure (!x + !y)
+
+The notation ``!expr`` means that the expression ``expr`` should be
+evaluated and then implicitly bound. Conceptually, we can think of
+``!`` as being a prefix function with the following type:
+
+.. code-block:: idris
+
+    (!) : m a -> a
+
+Note, however, that it is not really a function, merely syntax! In
+practice, a subexpression ``!expr`` will lift ``expr`` as high as
+possible within its current scope, bind it to a fresh name ``x``, and
+replace ``!expr`` with ``x``. Expressions are lifted depth first, left
+to right. In practice, ``!``-notation allows us to program in a more
+direct style, while still giving a notational clue as to which
+expressions are monadic.
+
+For example, the expression:
+
+.. code-block:: idris
+
+    let y = 94 in f !(g !(print y) !x)
+
+is lifted to:
+
+.. code-block:: idris
+
+    let y = 94 in do y' <- print y
+                     x' <- x
+                     g' <- g y' x'
+                     f g'
+
+Monad comprehensions
+~~~~~~~~~~~~~~~~~~~~
+
+The list comprehension notation we saw in Section
+:ref:`sect-more-expr` is more general, and applies to anything which
+has an implementation of both ``Monad`` and ``Alternative``:
+
+.. code-block:: idris
+
+    interface Applicative f => Alternative (f : Type -> Type) where
+        empty : f a
+        (<|>) : f a -> f a -> f a
+
+In general, a comprehension takes the form ``[ exp | qual1, qual2, …,
+qualn ]`` where ``quali`` can be one of:
+
+- A generator ``x <- e``
+
+- A *guard*, which is an expression of type ``Bool``
+
+- A let binding ``let x = e``
+
+To translate a comprehension ``[exp | qual1, qual2, …, qualn]``, first
+any qualifier ``qual`` which is a *guard* is translated to ``guard
+qual``, using the following function:
+
+.. code-block:: idris
+
+    guard : Alternative f => Bool -> f ()
+
+Then the comprehension is converted to ``do`` notation:
+
+.. code-block:: idris
+
+    do { qual1; qual2; ...; qualn; pure exp; }
+
+Using monad comprehensions, an alternative definition for ``m_add``
+would be:
+
+.. code-block:: idris
+
+    m_add : Maybe Int -> Maybe Int -> Maybe Int
+    m_add x y = [ x' + y' | x' <- x, y' <- y ]
+
+Idiom brackets
+==============
+
+While ``do`` notation gives an alternative meaning to sequencing,
+idioms give an alternative meaning to *application*. The notation and
+larger example in this section is inspired by Conor McBride and Ross
+Paterson’s paper “Applicative Programming with Effects” [#ConorRoss]_.
+
+First, let us revisit ``m_add`` above. All it is really doing is
+applying an operator to two values extracted from ``Maybe Int``. We
+could abstract out the application:
+
+.. code-block:: idris
+
+    m_app : Maybe (a -> b) -> Maybe a -> Maybe b
+    m_app (Just f) (Just a) = Just (f a)
+    m_app _        _        = Nothing
+
+Using this, we can write an alternative ``m_add`` which uses this
+alternative notion of function application, with explicit calls to
+``m_app``:
+
+.. code-block:: idris
+
+    m_add' : Maybe Int -> Maybe Int -> Maybe Int
+    m_add' x y = m_app (m_app (Just (+)) x) y
+
+Rather than having to insert ``m_app`` everywhere there is an
+application, we can use idiom brackets to do the job for us.
+To do this, we can give ``Maybe`` an implementation of ``Applicative``
+as follows, where ``<*>`` is defined in the same way as ``m_app``
+above (this is defined in the Idris library):
+
+.. code-block:: idris
+
+    Applicative Maybe where
+        pure = Just
+
+        (Just f) <*> (Just a) = Just (f a)
+        _        <*> _        = Nothing
+
+Using ``<*>`` we can use this implementation as follows, where a function
+application ``[ f a1 …an |]`` is translated into ``pure f <*> a1 <*>
+… <*> an``:
+
+.. code-block:: idris
+
+    m_add' : Maybe Int -> Maybe Int -> Maybe Int
+    m_add' x y = [ x + y |]
+
+An error-handling interpreter
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Idiom notation is commonly useful when defining evaluators. McBride
+and Paterson describe such an evaluator [#ConorRoss]_, for a language similar
+to the following:
+
+.. code-block:: idris
+
+    data Expr = Var String      -- variables
+              | Val Int         -- values
+              | Add Expr Expr   -- addition
+
+Evaluation will take place relative to a context mapping variables
+(represented as ``String``\s) to ``Int`` values, and can possibly fail.
+We define a data type ``Eval`` to wrap an evaluator:
+
+.. code-block:: idris
+
+    data Eval : Type -> Type where
+         MkEval : (List (String, Int) -> Maybe a) -> Eval a
+
+Wrapping the evaluator in a data type means we will be able to provide
+implementations of interfaces for it later. We begin by defining a function to
+retrieve values from the context during evaluation:
+
+.. code-block:: idris
+
+    fetch : String -> Eval Int
+    fetch x = MkEval (\e => fetchVal e) where
+        fetchVal : List (String, Int) -> Maybe Int
+        fetchVal [] = Nothing
+        fetchVal ((v, val) :: xs) = if (x == v)
+                                      then (Just val)
+                                      else (fetchVal xs)
+
+When defining an evaluator for the language, we will be applying functions in
+the context of an ``Eval``, so it is natural to give ``Eval`` an implementation
+of ``Applicative``. Before ``Eval`` can have an implementation of
+``Applicative`` it is necessary for ``Eval`` to have an implementation of
+``Functor``:
+
+.. code-block:: idris
+
+    Functor Eval where
+        map f (MkEval g) = MkEval (\e => map f (g e))
+
+    Applicative Eval where
+        pure x = MkEval (\e => Just x)
+
+        (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
+            app : Maybe (a -> b) -> Maybe a -> Maybe b
+            app (Just fx) (Just gx) = Just (fx gx)
+            app _         _         = Nothing
+
+Evaluating an expression can now make use of the idiomatic application
+to handle errors:
+
+.. code-block:: idris
+
+    eval : Expr -> Eval Int
+    eval (Var x)   = fetch x
+    eval (Val x)   = [| x |]
+    eval (Add x y) = [| eval x + eval y |]
+
+    runEval : List (String, Int) -> Expr -> Maybe Int
+    runEval env e = case eval e of
+        MkEval envFn => envFn env
+
+For example:
+
+::
+
+    InterpE> runEval [("x", 10), ("y",84)] (Add (Var "x") (Var "y"))
+    Just 94
+    InterpE> runEval [("x", 10), ("y",84)] (Add (Var "x") (Var "z"))
+    Nothing
+
+Named Implementations
+=====================
+
+It can be desirable to have multiple implementations of an interface for the
+same type, for example to provide alternative methods for sorting or printing
+values. To achieve this, implementations can be *named* as follows:
+
+.. code-block:: idris
+
+    [myord] Ord Nat where
+       compare Z (S n)     = GT
+       compare (S n) Z     = LT
+       compare Z Z         = EQ
+       compare (S x) (S y) = compare @{myord} x y
+
+This declares an implementation as normal, but with an explicit name,
+``myord``. The syntax ``compare @{myord}`` gives an explicit implementation to
+``compare``, otherwise it would use the default implementation for ``Nat``. We
+can use this, for example, to sort a list of ``Nat`` in reverse.
+Given the following list:
+
+.. code-block:: idris
+
+    testList : List Nat
+    testList = [3,4,1]
+
+We can sort it using the default ``Ord`` implementation, by using the ``sort``
+function available with ``import Data.List``, then we can try with the named
+implementation ``myord`` as follows, at the Idris prompt:
+
+::
+
+    Main> show (sort testList)
+    "[1, 3, 4]"
+    Main> show (sort @{myord} testList)
+    "[4, 3, 1]"
+
+Sometimes, we also need access to a named parent implementation. For example,
+the prelude defines the following ``Semigroup`` interface:
+
+.. code-block:: idris
+
+    interface Semigroup ty where
+      (<+>) : ty -> ty -> ty
+
+Then it defines ``Monoid``, which extends ``Semigroup`` with a “neutral”
+value:
+
+.. code-block:: idris
+
+    interface Semigroup ty => Monoid ty where
+      neutral : ty
+
+We can define two different implementations of ``Semigroup`` and
+``Monoid`` for ``Nat``, one based on addition and one on multiplication:
+
+.. code-block:: idris
+
+    [PlusNatSemi] Semigroup Nat where
+      (<+>) x y = x + y
+
+    [MultNatSemi] Semigroup Nat where
+      (<+>) x y = x * y
+
+The neutral value for addition is ``0``, but the neutral value for multiplication
+is ``1``. It's important, therefore, that when we define implementations
+of ``Monoid`` they extend the correct ``Semigroup`` implementation. We can
+do this with a ``using`` clause in the implementation as follows:
+
+.. code-block:: idris
+
+    [PlusNatMonoid] Monoid Nat using PlusNatSemi where
+      neutral = 0
+
+    [MultNatMonoid] Monoid Nat using MultNatSemi where
+      neutral = 1
+
+The ``using PlusNatSemi`` clause indicates that ``PlusNatMonoid`` should
+extend ``PlusNatSemi`` specifically.
+
+Determining Parameters
+======================
+
+When an interface has more than one parameter, it can help resolution if the
+parameters used to find an implementation are restricted. For example:
+
+.. code-block:: idris
+
+    interface Monad m => MonadState s (m : Type -> Type) | m where
+      get : m s
+      put : s -> m ()
+
+In this interface, only ``m`` needs to be known to find an implementation of
+this interface, and ``s`` can then be determined from the implementation. This
+is declared with the ``| m`` after the interface declaration. We call ``m`` a
+*determining parameter* of the ``MonadState`` interface, because it is the
+parameter used to find an implementation.
+
+
+.. [#ConorRoss] Conor McBride and Ross Paterson. 2008. Applicative programming
+       with effects. J. Funct. Program. 18, 1 (January 2008),
+       1-13. DOI=10.1017/S0956796807006326
+       http://dx.doi.org/10.1017/S0956796807006326

docs/source/tutorial/interp.rst

@@ -0,0 +1,292 @@
+.. _sect-interp:
+
+***********************************
+Example: The Well-Typed Interpreter
+***********************************
+
+In this section, we’ll use the features we’ve seen so far to write a
+larger example, an interpreter for a simple functional programming
+language, with variables, function application, binary operators and
+an ``if...then...else`` construct. We will use the dependent type
+system to ensure that any programs which can be represented are
+well-typed.
+
+Representing Languages
+======================
+
+First, let us define the types in the language. We have integers,
+booleans, and functions, represented by ``Ty``:
+
+.. code-block:: idris
+
+    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
+calculated just like any other value:
+
+.. code-block:: idris
+
+    interpTy : Ty -> Type
+    interpTy TyInt       = Integer
+    interpTy TyBool      = Bool
+    interpTy (TyFun a t) = interpTy a -> interpTy t
+
+We're going to define a representation of our language in such a way
+that only well-typed programs can be represented. We'll index the
+representations of expressions by their type, **and** the types of
+local variables (the context). The context can be represented using
+the ``Vect`` data type, so we'll need to import ``Data.Vect`` at the top of our
+source file:
+
+.. code-block:: idris
+
+    import Data.Vect
+
+Expressions are indexed by the types of the local
+variables, and the type of the expression itself:
+
+.. code-block:: idris
+
+    data Expr : Vect n Ty -> Ty -> Type
+
+The full representation of expressions is:
+
+.. code-block:: idris
+
+    data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
+        Stop : HasType FZ (t :: ctxt) t
+        Pop  : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t
+
+    data Expr : Vect n Ty -> Ty -> Type where
+        Var : HasType i ctxt t -> Expr ctxt t
+        Val : (x : Integer) -> Expr ctxt TyInt
+        Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)
+        App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t
+        Op  : (interpTy a -> interpTy b -> interpTy c) ->
+              Expr ctxt a -> Expr ctxt b -> Expr ctxt c
+        If  : Expr ctxt TyBool ->
+              Lazy (Expr ctxt a) ->
+              Lazy (Expr ctxt a) -> Expr ctxt a
+
+The code above makes use of the ``Vect`` and ``Fin`` types from the
+base libraries. ``Fin`` is available as part of ``Data.Vect``. Throughout,
+``ctxt`` refers to the local variable context.
+
+Since expressions are indexed by their type, we can read the typing
+rules of the language from the definitions of the constructors. Let us
+look at each constructor in turn.
+
+We use a nameless representation for variables — they are *de Bruijn
+indexed*. Variables are represented by a proof of their membership in
+the context, ``HasType i ctxt T``, which is a proof that variable ``i``
+in context ``ctxt`` has type ``T``. This is defined as follows:
+
+.. code-block:: idris
+
+    data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
+        Stop : HasType FZ (t :: ctxt) t
+        Pop  : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t
+
+We can treat *Stop* as a proof that the most recently defined variable
+is well-typed, and *Pop n* as a proof that, if the ``n``\ th most
+recently defined variable is well-typed, so is the ``n+1``\ th. In
+practice, this means we use ``Stop`` to refer to the most recently
+defined variable, ``Pop Stop`` to refer to the next, and so on, via
+the ``Var`` constructor:
+
+.. code-block:: idris
+
+    Var : HasType i ctxt t -> Expr ctxt t
+
+So, in an expression ``\x. \y. x y``, the variable ``x`` would have a
+de Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``,
+represented as ``Stop``. We find these by counting the number of
+lambdas between the definition and the use.
+
+A value carries a concrete representation of an integer:
+
+.. code-block:: idris
+
+    Val : (x : Integer) -> Expr ctxt TyInt
+
+A lambda creates a function. In the scope of a function of type ``a ->
+t``, there is a new local variable of type ``a``, which is expressed
+by the context index:
+
+.. code-block:: idris
+
+    Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)
+
+Function application produces a value of type ``t`` given a function
+from ``a`` to ``t`` and a value of type ``a``:
+
+.. code-block:: idris
+
+    App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t
+
+We allow arbitrary binary operators, where the type of the operator
+informs what the types of the arguments must be:
+
+.. code-block:: idris
+
+    Op : (interpTy a -> interpTy b -> interpTy c) ->
+         Expr ctxt a -> Expr ctxt b -> Expr ctxt c
+
+Finally, ``If`` expressions make a choice given a boolean. Each branch
+must have the same type, and we will evaluate the branches lazily so
+that only the branch which is taken need be evaluated:
+
+.. code-block:: idris
+
+    If : Expr ctxt TyBool ->
+         Lazy (Expr ctxt a) ->
+         Lazy (Expr ctxt a) ->
+         Expr ctxt a
+
+Writing the Interpreter
+=======================
+
+When we evaluate an ``Expr``, we'll need to know the values in scope,
+as well as their types. ``Env`` is an environment, indexed over the
+types in scope. Since an environment is just another form of list,
+albeit with a strongly specified connection to the vector of local
+variable types, we use the usual ``::`` and ``Nil`` constructors so
+that we can use the usual list syntax. Given a proof that a variable
+is defined in the context, we can then produce a value from the
+environment:
+
+.. code-block:: idris
+
+    data Env : Vect n Ty -> Type where
+        Nil  : Env Nil
+        (::) : interpTy a -> Env ctxt -> Env (a :: ctxt)
+
+    lookup : HasType i ctxt t -> Env ctxt -> interpTy t
+    lookup Stop    (x :: xs) = x
+    lookup (Pop k) (x :: xs) = lookup k xs
+
+Given this, an interpreter is a function which
+translates an ``Expr`` into a concrete Idris value with respect to a
+specific environment:
+
+.. code-block:: idris
+
+    interp : Env ctxt -> Expr ctxt t -> interpTy t
+
+The complete interpreter is defined as follows, for reference. For
+each constructor, we translate it into the corresponding Idris value:
+
+.. code-block:: idris
+
+    interp env (Var i)     = lookup i env
+    interp env (Val x)     = x
+    interp env (Lam sc)    = \x => interp (x :: env) sc
+    interp env (App f s)   = interp env f (interp env s)
+    interp env (Op op x y) = op (interp env x) (interp env y)
+    interp env (If x t e)  = if interp env x then interp env t
+                                             else interp env e
+
+Let us look at each case in turn. To translate a variable, we simply look it
+up in the environment:
+
+.. code-block:: idris
+
+    interp env (Var i) = lookup i env
+
+To translate a value, we just return the concrete representation of the
+value:
+
+.. code-block:: idris
+
+    interp env (Val x) = x
+
+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:
+
+.. code-block:: idris
+
+    interp env (Lam sc) = \x => interp (x :: env) sc
+
+For an application, we interpret the function and its argument and apply
+it directly. We know that interpreting ``f`` must produce a function,
+because of its type:
+
+.. code-block:: idris
+
+    interp env (App f s) = interp env f (interp env s)
+
+Operators and conditionals 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
+``if...then...else`` construct directly.
+
+.. code-block:: idris
+
+    interp env (Op op x y) = op (interp env x) (interp env y)
+    interp env (If x t e)  = if interp env x then interp env t
+                                             else interp env e
+
+Testing
+=======
+
+We can make some simple test functions. Firstly, adding two inputs
+``\x. \y. y + x`` is written as follows:
+
+.. code-block:: idris
+
+    add : Expr ctxt (TyFun TyInt (TyFun TyInt TyInt))
+    add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
+
+More interestingly, a factorial function ``fact``
+(e.g. ``\x. if (x == 0) then 1 else (fact (x-1) * x)``),
+can be written as:
+
+.. code-block:: idris
+
+    fact : Expr ctxt (TyFun TyInt TyInt)
+    fact = Lam (If (Op (==) (Var Stop) (Val 0))
+                   (Val 1)
+                   (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
+                           (Var Stop)))
+
+Running
+=======
+
+To finish, we write a ``main`` program which interprets the factorial
+function on user input:
+
+.. code-block:: idris
+
+    main : IO ()
+    main = do putStr "Enter a number: "
+              x <- getLine
+              printLn (interp [] fact (cast x))
+
+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:
+
+.. _factrun:
+.. literalinclude:: ../listing/idris-prompt-interp.txt
+
+
+Aside: ``cast``
+---------------
+
+The prelude defines an interface ``Cast`` which allows conversion
+between types:
+
+.. code-block:: idris
+
+    interface Cast from to where
+        cast : from -> to
+
+It is a *multi-parameter* interface, defining the source type and
+object type of the cast. It must be possible for the type checker to
+infer *both* parameters at the point where the cast is applied. There
+are casts defined between all of the primitive types, as far as they
+make sense.

docs/source/tutorial/introduction.rst

@@ -0,0 +1,75 @@
+.. _sect-intro:
+
+************
+Introduction
+************
+
+In conventional programming languages, there is a clear distinction
+between *types* and *values*. For example, in `Haskell
+<http://www.haskell.org>`_, the following are types, representing
+integers, characters, lists of characters, and lists of any value
+respectively:
+
+-  ``Int``, ``Char``, ``[Char]``, ``[a]``
+
+Correspondingly, the following values are examples of inhabitants of
+those types:
+
+-  ``42``, ``’a’``, ``"Hello world!"``, ``[2,3,4,5,6]``
+
+In a language with *dependent types*, however, the distinction is less
+clear. Dependent types allow types to “depend” on values — in other
+words, types are a *first class* language construct and can be
+manipulated like any other value. The standard example is the type of
+lists of a given length [#fn1]_, ``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, for example the length of a list, the type of a function
+can begin to describe its own properties. Take for example the
+concatenation 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
+
+    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
+project is to build a dependently typed language suitable for
+verifiable general purpose 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 libraries.
+
+Intended Audience
+=================
+
+This tutorial is intended as a brief introduction to the language, and
+is aimed at readers already familiar with a functional language such
+as `Haskell <http://www.haskell.org>`_ or `OCaml <http://ocaml.org>`_.
+In particular, a certain amount of familiarity with Haskell syntax is
+assumed, although most concepts will at least be explained
+briefly. The reader is also assumed to have some interest in using
+dependent types for writing and verifying software.
+
+For a more in-depth introduction to Idris, which proceeds at a much slower
+pace, covering interactive program development, with many more examples, see
+`Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_
+by Edwin Brady, available from `Manning <https://www.manning.com>`_.
+
+Example Code
+============
+
+This tutorial includes some example code, which has been tested
+against Idris 2. These files are available with the Idris 2 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.
+
+.. rubric:: Footnotes
+
+.. [#fn1] Typically, and perhaps confusingly, referred to in the dependently
+   typed programming literature as "vectors".

docs/source/tutorial/miscellany.rst

@@ -0,0 +1,165 @@
+.. _sect-misc:
+
+**********
+Miscellany
+**********
+
+In this section we discuss a variety of additional features:
+
++ auto, implicit, and default arguments;
++ literate programming; and
++ the universe hierarchy.
+
+Implicit arguments
+==================
+
+We have already seen implicit arguments, which allows arguments to be
+omitted when they can be inferred by the type checker [#IdrisType]_, e.g.
+
+.. code-block:: idris
+
+    index : forall a, n . Fin n -> Vect n a -> a
+
+Auto implicit arguments
+-----------------------
+
+In other situations, it may be possible to infer arguments not by type
+checking but by searching the context for an appropriate value, or
+constructing a proof. For example, the following definition of ``head``
+which requires a proof that the list is non-empty:
+
+.. code-block:: idris
+
+    isCons : List a -> Bool
+    isCons [] = False
+    isCons (x :: xs) = True
+
+    head : (xs : List a) -> (isCons xs = True) -> a
+    head (x :: xs) _ = x
+
+If the list is statically known to be non-empty, either because its
+value is known or because a proof already exists in the context, the
+proof can be constructed automatically. Auto implicit arguments allow
+this to happen silently. We define ``head`` as follows:
+
+.. code-block:: idris
+
+    head : (xs : List a) -> {auto p : isCons xs = True} -> a
+    head (x :: xs) = x
+
+The ``auto`` annotation on the implicit argument means that Idris
+will attempt to fill in the implicit argument by searching for a value
+of the appropriate type. In fact, internally, this is exactly how interface
+resolution works. It will try the following, in order:
+
+- Local variables, i.e. names bound in pattern matches or ``let`` bindings,
+  with exactly the right type.
+- The constructors of the required type. If they have arguments, it will
+  search recursively up to a maximum depth of 100.
+- Local variables with function types, searching recursively for the
+  arguments.
+- Any function with the appropriate return type which is marked with the
+  ``%hint`` annotation.
+
+In the case that a proof is not found, it can be provided explicitly as normal:
+
+.. code-block:: idris
+
+    head xs {p = ?headProof}
+
+Default implicit arguments
+---------------------------
+
+Besides having Idris automatically find a value of a given type, sometimes we
+want to have an implicit argument with a specific default value. In Idris, we can
+do this using the ``default`` annotation. While this is primarily intended to assist
+in automatically constructing a proof where auto fails, or finds an unhelpful value,
+it might be easier to first consider a simpler case, not involving proofs.
+
+If we want to compute the n'th fibonacci number (and defining the 0th fibonacci
+number as 0), we could write:
+
+.. code-block:: idris
+
+	fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
+	fibonacci {lag} Z = lag
+	fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
+
+After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``,
+and will return the 5th fibonacci number. Note that while this works, this is not the
+intended use of the ``default`` annotation. It is included here for illustrative purposes
+only. Usually, ``default`` is used to provide things like a custom proof search script.
+
+Literate programming
+====================
+
+[NOT YET IN IDRIS 2]
+
+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:
+
+.. code-block:: literate-idris
+   :force:
+
+    > module literate
+
+    This is a comment. The main program is below
+
+    > main : IO ()
+    > main = putStrLn "Hello literate world!\n"
+
+An additional restriction is that there must be a blank line between a
+program line (beginning with ``>``) and a comment line (beginning with
+any other character).
+
+Cumulativity
+============
+
+[NOT YET IN IDRIS 2]
+
+Since values can appear in types and *vice versa*, it is natural that
+types themselves have types. For example:
+
+::
+
+    *universe> :t Nat
+    Nat : Type
+    *universe> :t Vect
+    Vect : Nat -> Type -> Type
+
+But what about the type of ``Type``? If we ask Idris it reports:
+
+::
+
+    *universe> :t Type
+    Type : Type 1
+
+If ``Type`` were its own type, it would lead to an inconsistency due to
+`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,
+so internally there is a *hierarchy* of types (or *universes*):
+
+.. code-block:: idris
+
+    Type : Type 1 : Type 2 : Type 3 : ...
+
+Universes are *cumulative*, that is, if ``x : Type n`` we can also have
+that ``x : Type m``, as long as ``n < m``. The typechecker generates
+such universe constraints and reports an error if any inconsistencies
+are found. Ordinarily, a programmer does not need to worry about this,
+but it does prevent (contrived) programs such as the following:
+
+.. code-block:: idris
+
+    myid : (a : Type) -> a -> a
+    myid _ x = x
+
+    idid :  (a : Type) -> a -> a
+    idid = myid _ myid
+
+The application of ``myid`` to itself leads to a cycle in the universe
+hierarchy — ``myid``\ ’s first argument is a ``Type``, which cannot be
+at a lower level than required if it is applied to itself.
+
+.. [#IdrisType] https://github.com/david-christiansen/idris-type-providers

docs/source/tutorial/modules.rst

@@ -0,0 +1,249 @@
+.. _sect-namespaces:
+
+**********************
+Modules and Namespaces
+**********************
+
+An Idris program consists of a collection of modules. Each module
+includes an optional ``module`` declaration giving the name of the
+module, a list of ``import`` statements giving the other modules which
+are to be imported, and a collection of declarations and definitions of
+types, interfaces and functions. For example, the listing below gives a
+module which defines a binary tree type ``BTree`` (in a file
+``BTree.idr``):
+
+.. code-block:: idris
+
+    module BTree
+
+    public export
+    data BTree a = Leaf
+                 | Node (BTree a) a (BTree a)
+
+    export
+    insert : Ord a => a -> BTree a -> BTree a
+    insert x Leaf = Node Leaf x Leaf
+    insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
+                                       else (Node l v (insert x r))
+
+    export
+    toList : BTree a -> List a
+    toList Leaf = []
+    toList (Node l v r) = BTree.toList l ++ (v :: BTree.toList r)
+
+    export
+    toTree : Ord a => List a -> BTree a
+    toTree [] = Leaf
+    toTree (x :: xs) = insert x (toTree xs)
+
+The modifiers ``export`` and ``public export`` say which names are visible
+from other namespaces. These are explained further below.
+
+Then, this gives a main program (in a file
+``bmain.idr``) which uses the ``BTree`` module to sort a list:
+
+.. code-block:: idris
+
+    module Main
+
+    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: 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``
+
+If names are otherwise unambiguous, there is no need to give the fully
+qualified name. Names can be disambiguated either by giving an explicit
+qualification, or according to their type.
+
+There is no formal link between the module name and its filename,
+although it is generally advisable to use the same name for each. An
+``import`` statement refers to a filename, using dots to separate
+directories. For example, ``import foo.bar`` would import the file
+``foo/bar.idr``, which would conventionally have the module declaration
+``module foo.bar``. The only requirement for module names is that the
+main module, with the ``main`` function, must be called
+``Main`` — although its filename need not be ``Main.idr``.
+
+Export Modifiers
+================
+
+Idris allows for fine-grained control over the visibility of a
+namespace's contents. By default, all names defined in a namespace are kept
+private.  This aids in specification of a minimal interface and for
+internal details to be left hidden. Idris allows for functions,
+types, and interfaces to be marked as: ``private``, ``export``, or
+``public export``. Their general meaning is as follows:
+
+- ``private`` meaning that it is not exported at all. This is the default.
+
+- ``export`` meaning that its top level type is exported.
+
+- ``public export`` meaning that the entire definition is exported.
+
+A further restriction in modifying the visibility is that definitions must not
+refer to anything within a lower level of visibility. For example, ``public
+export`` definitions cannot use ``private`` or ``export`` names, and ``export``
+types cannot use ``private`` names. This is to prevent private names leaking
+into a module's interface.
+
+Meaning for Functions
+---------------------
+
+- ``export`` the type is exported
+
+- ``public export`` the type and definition are exported, and the
+  definition can be used after it is imported. In other words, the
+  definition itself is considered part of the module's interface. The
+  long name ``public export`` is intended to make you think twice
+  about doing this.
+
+.. note::
+
+   Type synonyms in Idris are created by writing a function. When
+   setting the visibility for a module, it is usually a good idea to
+   ``public export`` all type synonyms if they are to be used outside
+   the module. Otherwise, Idris won't know what the synonym is a
+   synonym for.
+
+Since ``public export`` means that a function's definition is exported,
+this effectively makes the function definition part of the module's API.
+Therefore, it's generally a good idea to avoid using ``public export`` for
+functions unless you really mean to export the full definition.
+
+Meaning for Data Types
+----------------------
+
+For data types, the meanings are:
+
+- ``export`` the type constructor is exported
+
+- ``public export`` the type constructor and data constructors are exported
+
+
+Meaning for Interfaces
+----------------------
+
+For interfaces, the meanings are:
+
+- ``export`` the interface name is exported
+
+- ``public export`` the interface name, method names and default
+  definitions are exported
+
+Propagating Inner Module API's
+-------------------------------
+
+Additionally, a module can re-export a module it has imported, by using
+the ``public`` modifier on an ``import``. For example:
+
+.. code-block:: idris
+   :force:
+
+    module A
+
+    import B
+    import public C
+
+The module ``A`` will export the name ``a``, as well as any public or
+abstract names in module ``C``, but will not re-export anything from
+module ``B``.
+
+Explicit Namespaces
+===================
+
+Defining a module also defines a namespace implicitly. However,
+namespaces can also be given *explicitly*. This is most useful if you
+wish to overload names within the same module:
+
+.. code-block:: idris
+
+    module Foo
+
+    namespace X
+      export
+      test : Int -> Int
+      test x = x * 2
+
+    namespace Y
+      export
+      test : String -> String
+      test x = x ++ x
+
+This (admittedly contrived) module defines two functions with fully
+qualified names ``Foo.X.test`` and ``Foo.Y.test``, which can be
+disambiguated by their types:
+
+::
+
+    *Foo> test 3
+    6 : Int
+    *Foo> test "foo"
+    "foofoo" : String
+
+The export rules, ``public export`` and ``export``, are *per namespace*,
+not *per file*, so the two ``test`` definitions above need the ``export``
+flag to be visible outside their own namespaces.
+
+Parameterised blocks
+====================
+
+Groups of functions can be parameterised over a number of arguments
+using a ``parameters`` declaration, for example:
+
+.. code-block:: idris
+
+    parameters (x : Nat, y : Nat)
+      addAll : Nat -> Nat
+      addAll z = x + y + z
+
+The effect of a ``parameters`` block is to add the declared parameters
+to every function, type and data constructor within the
+block. Specifically, adding the parameters to the front of the
+argument list. Outside the block, the parameters must be given
+explicitly. The ``addAll`` function, when called from the REPL, will
+thus have the following type signature.
+
+::
+
+    *params> :t addAll
+    addAll : Nat -> Nat -> Nat -> Nat
+
+and the following definition.
+
+.. code-block:: idris
+
+    addAll : (x : Nat) -> (y : Nat) -> (z : Nat) -> Nat
+    addAll x y z = x + y + z
+
+Parameters blocks can be nested, and can also include data declarations,
+in which case the parameters are added explicitly to all type and data
+constructors. They may also be dependent types with implicit arguments:
+
+.. code-block:: idris
+
+    parameters (y : Nat, xs : Vect x a)
+      data Vects : Type -> Type where
+        MkVects : Vect y a -> Vects a
+
+      append : Vects a -> Vect (x + y) a
+      append (MkVects ys) = xs ++ ys
+
+To use ``Vects`` or ``append`` outside the block, we must also give the
+``xs`` and ``y`` arguments. Here, we can use placeholders for the values
+which can be inferred by the type checker:
+
+::
+
+    Main> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))
+    "[1, 2, 3, 4, 5, 6]"

docs/source/tutorial/multiplicities.rst

@@ -0,0 +1,563 @@
+.. _sect-multiplicities:
+
+**************
+Multiplicities
+**************
+
+Idris 2 is
+based on `Quantitative Type Theory (QTT)
+<https://bentnib.org/quantitative-type-theory.html>`_, a core language
+developed by Bob Atkey and Conor McBride. In practice, this means that every
+variable in Idris 2 has a *quantity* associated with it. A quantity is one of:
+
+* ``0``, meaning that the variable is *erased* at run time
+* ``1``, meaning that the variable is used *exactly once* at run time
+* *Unrestricted*, which is the same behaviour as Idris 1
+
+We can see the multiplicities of variables by inspecting holes. For example,
+if we have the following skeleton definition of ``append`` on vectors...
+
+.. code-block:: idris
+
+    append : Vect n a -> Vect m a -> Vect (n + m) a
+    append xs ys = ?append_rhs
+
+...we can look at the hole ``append_rhs``:
+
+::
+
+    Main> :t append_rhs
+     0 m : Nat
+     0 a : Type
+     0 n : Nat
+       ys : Vect m a
+       xs : Vect n a
+    -------------------------------------
+    append_rhs : Vect (plus n m) a
+
+The ``0`` next to ``m``, ``a`` and ``n`` mean that they are in scope, but there
+will be ``0`` occurrences at run-time. That is, it is **guaranteed** that they
+will be erased at run-time.
+
+Multiplicities can be explicitly written in function types as follows:
+
+* ``ignoreN : (0 n : Nat) -> Vect n a -> Nat`` - this function cannot look at
+  ``n`` at run time
+* ``duplicate : (1 x : a) -> (a, a)`` - this function must use ``x`` exactly
+  once (so good luck implementing it, by the way. There is no implementation
+  because it would need to use ``x`` twice!)
+
+If there is no multiplicity annotation, the argument is unrestricted.
+If, on the other hand, a name is implicitly bound (like ``a`` in both examples above)
+the argument is erased. So, the above types could also be written as:
+
+* ``ignoreN : {0 a : _} -> (0 n : Nat) -> Vect n a -> Nat``
+* ``duplicate : {0 a : _} -> (1 x : a) -> (a, a)``
+
+This section describes what this means for your Idris 2 programs in practice,
+with several examples. In particular, it describes:
+
+* :ref:`sect-erasure` - how to know what is relevant at run time and what is erased
+* :ref:`sect-linearity` - using the type system to encode *resource usage protocols*
+* :ref:`sect-pmtypes` - truly first class types
+
+The most important of these for most programs, and the thing you'll need to
+know about if converting Idris 1 programs to work with Idris 2, is erasure_.
+The most interesting, however, and the thing which gives Idris 2 much more
+expressivity, is linearity_, so we'll start there.
+
+.. _sect-linearity:
+
+Linearity
+---------
+
+The ``1`` multiplicity expresses that a variable must be used exactly once.
+First, we'll see how this works on some small examples of functions and
+data types, then see how it can be used to encode `resource protocols`_.
+
+Above, we saw the type of ``duplicate``. Let's try to write it interactively,
+and see what goes wrong. We'll start by giving the type and a skeleton
+definition with a hole
+
+.. code-block:: idris
+
+    duplicate : (1 x : a) -> (a, a)
+    duplicate x = ?help
+
+Checking the type of a hole tells us the multiplicity of each variable in
+scope. If we check the type of ``?help`` we'll see that we can't
+use ``a`` at run time, and we have to use ``x`` exactly once::
+
+  Main> :t help
+   0 a : Type
+   1 x : a
+  -------------------------------------
+  help : (a, a)
+
+If we use ``x`` for one part of the pair...
+
+.. code-block:: idris
+
+    duplicate : (1 x : a) -> (a, a)
+    duplicate x = (x, ?help)
+
+...then the type of the remaining hole tells us we can't use it for the other::
+
+  Main> :t help
+   0 a : Type
+   0 x : a
+  -------------------------------------
+  help : a
+
+The same happens if we try defining ``duplicate x = (?help, x)`` (try it!)
+The intution behind multiplicity ``1`` is that if we have a function with
+a type of the following form...
+
+.. code-block:: idris
+
+    f : (1 x : a) -> b
+
+...then the guarantee given by the type system is that *if* ``f x`` *is used
+exactly once, then* ``x`` *is used exactly once*. So, if we insist on
+trying to define ``duplicate``...::
+
+  duplicate x = (x, x)
+
+...then Idris will complain::
+
+  pmtype.idr:2:15--8:1:While processing right hand side of Main.duplicate at pmtype.idr:2:1--8:1:
+  There are 2 uses of linear name x
+
+A similar intuition applies for data types. Consider the following types,
+``Lin`` which wraps an argument that must be used once, and ``Unr`` which
+wraps an argument with unrestricted use
+
+.. code-block:: idris
+
+    data Lin : Type -> Type where
+         MkLin : (1 x : a) -> Lin a
+  
+    data Unr : Type -> Type where
+         MkUnr : (x : a) -> Unr a
+  
+If ``MkLin x`` is used once, then ``x`` is used once. But if ``MkUnr x`` is
+used once, there is no guarantee on how often ``x`` is used. We can see this a
+bit more clearly by starting to write projection functions for ``Lin`` and
+``Unr`` to extract the argument
+
+.. code-block:: idris
+
+    getLin : (1 val : Lin a) -> a
+    getLin (MkLin x) = ?howmanyLin
+  
+    getUnr : (1 val : Unr a) -> a
+    getUnr (MkUnr x) = ?howmanyUnr
+  
+Checking the types of the holes shows us that, for ``getLin``, we must use
+``x`` exactly once (Because the ``val`` argument is used once,
+by pattern matching on it as ``MkLin x``, and if ``MkLin x`` is used once,
+``x`` must be used once)::
+
+  Main> :t howmanyLin
+   0 a : Type
+   1 x : a
+  -------------------------------------
+  howmanyLin : a
+
+For ``getUnr``, however, we still have to use ``val`` once, again by pattern
+matching on it, but using ``MkUnr x`` once doesn't place any restrictions on
+``x``. So, ``x`` has unrestricted use in the body of ``getUnr``::
+
+  Main> :t howmanyUnr
+   0 a : Type
+     x : a
+  -------------------------------------
+  howmanyUnr : a
+
+If ``getLin`` has an unrestricted argument...
+
+.. code-block:: idris
+
+    getLin : (val : Lin a) -> a
+    getLin (MkLin x) = ?howmanyLin
+
+...then ``x`` is unrestricted in ``howmanyLin``::
+  
+  Main> :t howmanyLin
+   0 a : Type
+     x : a
+  -------------------------------------
+  howmanyLin : a
+
+Remember the intuition from the type of ``MkLin`` is that if ``MkLin x`` is
+used exactly once, ``x`` is used exactly once. But, we didn't say that
+``MkLin x`` would be used exactly once, so there is no restriction on ``x``.
+
+Resource protocols
+~~~~~~~~~~~~~~~~~~
+
+One way to take advantage of being able to express linear usage of an argument
+is in defining resource usage protocols, where we can use linearity to ensure
+that any unique external resource has only one instance, and we can use
+functions which are linear in their arguments to represent state transitions on
+that resource. A door, for example, can be in one of two states, ``Open`` or
+``Closed``
+
+.. code-block:: idris
+
+    data DoorState = Open | Closed
+
+    data Door : DoorState -> Type where
+         MkDoor : (doorId : Int) -> Door st
+
+(Okay, we're just pretending here - imagine the ``doorId`` is a reference
+to an external resource!)
+
+We can define functions for opening and closing the door which explicitly
+describe how they change the state of a door, and that they are linear in
+the door
+
+.. code-block:: idris
+
+    openDoor : (1 d : Door Closed) -> Door Open
+    closeDoor : (1 d : Door Open) -> Door Closed
+
+Remember, the intuition is that if ``openDoor d`` is used exactly once,
+then ``d`` is used exactly once. So, provided that a door ``d`` has
+multiplicity ``1`` when it's created, we *know* that once we call
+``openDoor`` on it, we won't be able to use ``d`` again. Given that
+``d`` is an external resource, and ``openDoor`` has changed it's state,
+this is a good thing!
+
+We can ensure that any door we create has multiplicity ``1`` by
+creating them with a ``newDoor`` function with the following type
+
+.. code-block:: idris
+
+    newDoor : (1 p : (1 d : Door Closed) -> IO ()) -> IO ()
+
+That is, ``newDoor`` takes a function, which it runs exactly once. That
+function takes a door, which is used exactly once. We'll run it in
+``IO`` to suggest that there is some interaction with the outside world
+going on when we create the door. Since the multiplicity ``1`` means the
+door has to be used exactly once, we need to be able to delete the door
+when we're finished
+
+.. code-block:: idris
+
+    deleteDoor : (1 d : Door Closed) -> IO ()
+
+So an example correct door protocol usage would be
+
+.. code-block:: idris
+
+    doorProg : IO ()
+    doorProg 
+        = newDoor $ \d =>
+              let d' = openDoor d
+                  d'' = closeDoor d' in
+                  deleteDoor d''
+ 
+It's instructive to build this program interactively, with holes along
+the way, and see how the multiplicities of ``d``, ``d'`` etc change. For
+example
+
+.. code-block:: idris
+
+    doorProg : IO ()
+    doorProg 
+        = newDoor $ \d =>
+              let d' = openDoor d in
+                  ?whatnow
+
+Checking the type of ``?whatnow`` shows that ``d`` is now spent, but we
+still have to use ``d'`` exactly once::
+
+  Main> :t whatnow
+   0 d : Door Closed
+   1 d' : Door Open
+  -------------------------------------
+  whatnow : IO ()
+
+Note that the ``0`` multiplicity for ``d`` means that we can still *talk*
+about it - in particular, we can still reason about it in types - but we
+can't use it again in a relevant position in the rest of the program.
+It's also fine to shadow the name ``d`` throughout
+
+.. code-block:: idris
+
+    doorProg : IO ()
+    doorProg 
+        = newDoor $ \d =>
+              let d = openDoor d
+                  d = closeDoor d in
+                  deleteDoor d
+
+If we don't follow the protocol correctly - create the door, open it, close
+it, then delete it - then the program won't type check. For example, we
+can try not to delete the door before finishing
+
+.. code-block:: idris
+
+    doorProg : IO ()
+    doorProg 
+        = newDoor $ \d =>
+              let d' = openDoor d
+                  d'' = closeDoor d' in
+                  putStrLn "What could possibly go wrong?"
+
+This gives the following error::
+
+  Door.idr:15:19--15:38:While processing right hand side of Main.doorProg at Door.idr:13:1--17:1:
+  There are 0 uses of linear name d''
+
+There's a lot more to be said about the details here! But, this shows at
+a high level how we can use linearity to capture resource usage protocols
+at the type level. If we have an external resource which is guaranteed to
+be used linearly, like ``Door``, we don't need to run operations on that
+resource in an ``IO`` monad, since we're already enforcing an ordering on
+operations and don't have access to any out of date resource states. This is
+similar to the way interactive programs work in 
+`the Clean programming language <https://clean.cs.ru.nl/Clean>`_, and in
+fact is how ``IO`` is implemented internally in Idris 2, with a special
+``%World`` type for representing the state of the outside world that is
+always used linearly
+
+.. code-block:: idris
+
+    public export
+    data IORes : Type -> Type where
+         MkIORes : (result : a) -> (1 x : %World) -> IORes a
+
+    export
+    data IO : Type -> Type where
+         MkIO : (1 fn : (1 x : %World) -> IORes a) -> IO a
+
+Having multiplicities in the type system raises several interesting
+questions, such as:
+
+* Can we use linearity information to inform memory management and, for
+  example, have type level guarantees about functions which will not need
+  to perform garbage collection?
+* How should multiplicities be incorporated into interfaces such as
+  ``Functor``, ``Applicative`` and ``Monad``?
+* If we have ``0``, and ``1`` as multiplicities, why stop there? Why not have
+  ``2``, ``3`` and more (like `Granule
+  <https://granule-project.github.io/granule.html>`_)
+* What about multiplicity polymorphism, as in the `Linear Haskell proposal <https://arxiv.org/abs/1710.09756>`_?
+* Even without all of that, what can we do *now*?
+
+.. _sect-erasure:
+
+Erasure
+-------
+
+The ``1`` multiplicity give us many possibilities in the kinds of
+properties we can express. But, the ``0`` multiplicity is perhaps more
+important in that it allows us to be precise about which values are
+relevant at run time, and which are compile time only (that is, which are
+erased). Using the ``0`` multiplicity means a function's type now tells us
+exactly what it needs at run time.
+
+For example, in Idris 1 you could get the length of a vector as follows
+
+.. code-block:: idris
+
+    vlen : Vect n a -> Nat
+    vlen {n} xs = n
+  
+This is fine, since it runs in constant time, but the trade off is that
+``n`` has to be available at run time, so at run time we always need the length
+of the vector to be available if we ever call ``vlen``. Idris 1 can infer whether
+the length is needed, but there's no easy way for a programmer to be sure.
+
+In Idris 2, we need to state explicitly that ``n`` is needed at run time
+
+.. code-block:: idris
+
+    vlen : {n : Nat} -> Vect n a -> Nat
+    vlen xs = n
+  
+(Incidentally, also note that in Idris 2, names bound in types are also available
+in the definition without explicitly rebinding them.)
+
+This also means that when you call ``vlen``, you need the length available. For
+example, this will give an error
+
+.. code-block:: idris
+
+    sumLengths : Vect m a -> Vect n a —> Nat
+    sumLengths xs ys = vlen xs + vlen ys
+  
+Idris 2 reports::
+
+  vlen.idr:7:20--7:28:While processing right hand side of Main.sumLengths at vlen.idr:7:1--10:1:
+  m is not accessible in this context
+  
+This means that it needs to use ``m`` as an argument to pass to ``vlen xs``,
+where it needs to be available at run time, but ``m`` is not available in
+``sumLengths`` because it has multiplicity ``0``.
+
+We can see this more clearly by replacing the right hand side of
+``sumLengths`` with a hole...
+
+.. code-block:: idris
+
+    sumLengths : Vect m a -> Vect n a -> Nat
+    sumLengths xs ys = ?sumLengths_rhs
+  
+...then checking the hole's type at the REPL::
+
+  Main> :t sumLengths_rhs
+   0 n : Nat
+   0 a : Type
+   0 m : Nat
+     ys : Vect n a
+     xs : Vect m a
+  -------------------------------------
+  sumLengths_rhs : Nat
+
+Instead, we need to give bindings for ``m`` and ``n`` with
+unrestricted multiplicity
+
+.. code-block:: idris
+
+    sumLengths : {m, n : _} -> Vect m a -> Vect n a —> Nat
+    sumLengths xs ys = vLen xs + vLen xs
+
+Remember that giving no multiplicity on a binder, as with ``m`` and ``n`` here,
+means that the variable has unrestricted usage.
+
+If you're converting Idris 1 programs to work with Idris 2, this is probably the
+biggest thing you need to think about. It is important to note,
+though, that if you have bound implicits, such as...
+
+.. code-block:: idris
+
+    excitingFn : {t : _} -> Coffee t -> Moonbase t
+   
+...then it's a good idea to make sure ``t`` really is needed, or performance
+might suffer due to the run time building the instance of ``t`` unnecessarily!
+
+One final note on erasure: it is an error to try to pattern match on an
+argument with multiplicity ``0``, unless its value is inferrable from
+elsewhere. So, the following definition is rejected
+
+.. code-block:: idris
+
+    badNot : (0 x : Bool) -> Bool
+    badNot False = True
+    badNot True = False
+
+This is rejected with the error::
+
+  badnot.idr:2:1--3:1:Attempt to match on erased argument False in 
+  Main.badNot
+
+The following, however, is fine, because in ``sNot``, even though we appear
+to match on the erased argument ``x``, its value is uniquely inferrable from
+the type of the second argument
+
+.. code-block:: idris
+
+    data SBool : Bool -> Type where
+         SFalse : SBool False
+         STrue  : SBool True
+  
+    sNot : (0 x : Bool) -> SBool x -> Bool
+    sNot False SFalse = True
+    sNot True  STrue  = False
+
+Experience with Idris 2 so far suggests that, most of the time, as long as
+you're using unbound implicits in your Idris 1 programs, they will work without
+much modification in Idris 2. The Idris 2 type checker will point out where you
+require an unbound implicit argument at run time - sometimes this is both
+surprising and enlightening!
+
+.. _sect-pmtypes:
+
+Pattern Matching on Types
+-------------------------
+
+One way to think about dependent types is to think of them as "first class"
+objects in the language, in that they can be assigned to variables, 
+passed around and returned from functions, just like any other construct.
+But, if they're truly first class, we should be able to pattern match on
+them too! Idris 2 allows us to do this. For example
+
+.. code-block:: idris
+ 
+    showType : Type -> String
+    showType Int = "Int"
+    showType (List a) = "List of " ++ showType a
+    showType _ = "something else"
+
+We can try this as follows::
+
+  Main> showType Int
+  "Int"
+  Main> showType (List Int)
+  "List of Int"
+  Main> showType (List Bool)
+  "List of something else"
+
+Pattern matching on function types is interesting, because the return type
+may depend on the input value. For example, let's add a case to
+``showType``
+
+.. code-block:: idris
+
+  showType (Nat -> a) = ?help
+
+Inspecting the type of ``help`` tells us::
+
+  Main> :t help
+     a : Nat -> Type
+  -------------------------------------
+  help : String
+
+So, the return type ``a`` depends on the input value of type ``Nat``, and
+we'll need to come up with a value to use ``a``, for example
+
+.. code-block:: idris
+
+    showType (Nat -> a) = "Function from Nat to " ++ showType (a Z)
+
+Note that multiplicities on the binders, and the ability to pattern match
+on *non-erased* types mean that the following two types are distinct
+
+.. code-block:: idris
+
+    id : a -> a
+    notId : {a : Type} -> a -> a
+
+In the case of ``notId``, we can match on ``a`` and get a function which
+is certainly not the identity function
+
+.. code-block:: idris
+
+    notId {a = Int} x = x + 1
+    notId x = x
+
+::
+
+  Main> notId 93
+  94
+  Main> notId "???"
+  "???"
+
+There is an important consequence of being able to distinguish between relevant
+and irrelevant type arguments, which is that a function is *only* parametric in
+``a`` if ``a`` has multiplicity ``0``. So, in the case of ``notId``, ``a`` is
+*not* a parameter, and so we can't draw any conclusions about the way the
+function will behave because it is polymorphic, because the type tells us it
+might pattern match on ``a``.
+
+On the other hand, it is merely a coincidence that, in non-dependently typed
+languages, types are *irrelevant* and get erased, and values are *relevant*
+and remain at run time. Idris 2, being based on QTT, allows us to make the
+distinction between relevant and irrelevant arguments precise. Types can be
+relevant, values (such as the ``n`` index to vectors) can be irrelevant.
+
+For more details on multiplicities,
+see `Idris 2: Quantitative Type Theory in Action <https://www.type-driven.org.uk/edwinb/idris-2-quantitative-type-theory-in-action.html>`_.

docs/source/tutorial/packages.rst

@@ -0,0 +1,87 @@
+.. _sect-packages:
+
+********
+Packages
+********
+
+Idris includes a simple build system for building packages and executables
+from a named package description file. These files can be used with the
+Idris compiler to manage the development process.
+
+Package Descriptions
+====================
+
+A package description includes the following:
+
++ A header, consisting of the keyword ``package`` followed by a package
+  name. Package names can be any valid Idris identifier. The iPKG
+  format also takes a quoted version that accepts any valid filename.
+
++ Fields describing package contents, ``<field> = <value>``.
+
+At least one field must be the modules field, where the value is a
+comma separated list of modules. For example, given an idris package
+``maths`` that has modules ``Maths.idr``, ``Maths.NumOps.idr``,
+``Maths.BinOps.idr``, and ``Maths.HexOps.idr``, the corresponding
+package file would be:
+
+::
+
+    package maths
+
+    modules = Maths
+            , Maths.NumOps
+            , Maths.BinOps
+            , Maths.HexOps
+
+
+Other examples of package files can be found in the ``libs`` directory
+of the main Idris repository, and in `third-party libraries
+<https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
+
+
+Using Package files
+===================
+
+Idris itself is aware about packages, and special commands are
+available to help with, for example, building packages, installing
+packages, and cleaning packages.  For instance, given the ``maths``
+package from earlier we can use Idris as follows:
+
++ ``idris2 --build maths.ipkg`` will build all modules in the package
+
++ ``idris2 --install maths.ipkg`` will install the package, making it
+  accessible by other Idris libraries and programs.
+
++ ``idris2 --clean maths.ipkg`` will delete all intermediate code and
+  executable files generated when building.
+
+Once the maths package has been installed, the command line option
+``--package maths`` makes it accessible (abbreviated to ``-p maths``).
+For example:
+
+::
+
+    idris2 -p maths Main.idr
+
+Package Dependencies Using Atom
+===============================
+
+If you are using the Atom editor and have a dependency on another package,
+corresponding to for instance ``import Lightyear`` or ``import Pruviloj``,
+you need to let Atom know that it should be loaded. The easiest way to
+accomplish that is with a .ipkg file. The general contents of an ipkg file
+will be described in the next section of the tutorial, but for now here is
+a simple recipe for this trivial case:
+
+- Create a folder myProject.
+
+- Add a file myProject.ipkg containing just a couple of lines:
+
+.. code-block:: idris
+
+    package myProject
+
+    pkgs = pruviloj, lightyear
+
+- In Atom, use the File menu to Open Folder myProject.

docs/source/tutorial/starting.rst

@@ -0,0 +1,104 @@
+.. _sect-starting:
+
+***************
+Getting Started
+***************
+
+Prerequisites
+=============
+
+You need a C compiler (default is clang), and optionally Idris 1.3.2 to build
+from source. You will also need:
+
+- `Chez Scheme <https://cisco.github.io/ChezScheme/>`_
+- The `GNU Multiple Precision Arithmetic Library <https://gmplib.org/>`_ (GMP) 
+
+Both are available from MacPorts/Homebrew and all major Linux distributions.
+
+**Note**: If you install ChezScheme from source files, building it locally, make sure
+you run ``./configure --threads`` to build multithreading support in.
+
+Downloading and Installing
+==========================
+
+You can download the Idris 2 source from the `Idris web site
+<https://www.idris-lang.org/pages/download.html>`_. 
+This includes the Idris 2 source code (written in Idris 1) and the C
+code generated from that.  Once you have unpacked the source, you can
+install it as follows:
+
+* If you have Idris 1.3.2 installed::
+
+    make install
+
+* If not, you can install directly from the generated C::
+
+    make install-fromc
+
+This will, by default, install into ``${HOME}/.idris2``. You can change this
+by editing the options at the beginning of the ``Makefile``. For example,
+to install into ``/usr/local``, you can edit the ``PREFIX`` as follows::
+
+    PREFIX ?= /usr/local
+
+To check that installation has succeeded, and to write your first
+Idris program, create a file called ``hello.idr`` containing the
+following text:
+
+.. code-block:: idris
+
+    module Main
+
+    main : IO ()
+    main = putStrLn "Hello world"
+
+If you are familiar with Haskell, it should be fairly clear what the
+program is doing and how it works, but if not, we will explain the
+details later. You can compile the program to an executable by
+entering ``idris2 hello.idr -o hello`` at the shell prompt. This will,
+by default, create an executable called ``hello``, which invokes a generated
+and compiled Chez Schem program, in the destination directory ``build/exec``
+which you can run:
+
+::
+
+    $ idris2 hello.idr -o hello
+    compiling hello.ss with output to hello.so
+    $ ./build/exec/hello.so
+    Hello world
+
+Please note that the dollar sign ``$`` indicates the shell prompt!
+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.
+
+- ``--package pkg`` add package as dependency, e.g. ``--package contrib`` to make use of the contrib package.
+
+- ``--help`` display usage summary and command line options.
+
+You can find out more about compiling to executables in
+Section :ref:`sect-execs`.
+
+The Interactive Environment
+===========================
+
+Entering ``idris2`` at the shell prompt starts up the interactive
+environment. You should see something like the following:
+
+.. literalinclude:: ../listing/idris-prompt-start.txt
+
+This gives a ``ghci`` style interface which allows evaluation of, as
+well as type checking of, expressions; theorem proving, compilation;
+editing; and various other operations. The command ``:?`` gives a list
+of supported commands. Below, we see an example run in
+which ``hello.idr`` is loaded, the type of ``main`` is checked and
+then the program is compiled to the executable file ``hello``,
+available in the destination directory ``build/exec/``. Type
+checking a file, if successful, creates a bytecode version of the file (in this
+case ``build/ttc/hello.ttc``) to speed up loading in future. The bytecode is
+regenerated if the source file changes.
+
+.. _run1:
+.. literalinclude:: ../listing/idris-prompt-helloworld.txt

docs/source/tutorial/theorems.rst

@@ -0,0 +1,457 @@
+.. _sect-theorems:
+
+***************
+Theorem Proving
+***************
+
+Equality
+========
+
+Idris allows propositional equalities to be declared, allowing theorems about
+programs to be stated and proved. An equality type is defined as follows in the
+Prelude:
+
+.. code-block:: idris
+
+    data Equal : a -> b -> Type where
+         Refl : Equal x x
+
+As a notational convenience, ``Equal x y`` can be written as ``x = y``.
+Equalities can be proposed between any values of any types, but the only
+way to construct a proof of equality is if values actually are equal.
+For example:
+
+.. code-block:: idris
+
+    fiveIsFive : 5 = 5
+    fiveIsFive = Refl
+
+    twoPlusTwo : 2 + 2 = 4
+    twoPlusTwo = Refl
+
+If we try...
+
+.. code-block:: idris
+
+    twoPlusTwoBad : 2 + 2 = 5
+    twoPlusTwoBad = Refl
+
+...then we'll get an error:
+
+::
+
+    Proofs.idr:8:17--10:1:While processing right hand side of Main.twoPlusTwoBad at Proofs.idr:8:1--10:1:
+    When unifying 4 = 4 and (fromInteger 2 + fromInteger 2) = (fromInteger 5)
+    Mismatch between:
+            4
+    and
+            5
+
+.. _sect-empty:
+
+The Empty Type
+==============
+
+There is an empty type, ``Void``, which has no constructors. It is therefore
+impossible to construct a canonical element of the empty type. We can therefore
+use the empty type to prove that something is impossible, for example zero is
+never equal to a successor:
+
+.. code-block:: idris
+
+    disjoint : (n : Nat) -> Z = S n -> Void
+    disjoint n prf = replace {p = disjointTy} prf ()
+      where
+        disjointTy : Nat -> Type
+        disjointTy Z = ()
+        disjointTy (S k) = Void
+
+Don't worry if you don't get all the details of how this works just yet -
+essentially, it applies the library function ``replace``, which uses an
+equality proof to transform a predicate. Here we use it to transform a
+value of a type which can exist, the empty tuple, to a value of a type
+which can’t, by using a proof of something which can’t exist.
+
+Once we have an element of the empty type, we can prove anything.
+``void`` is defined in the library, to assist with proofs by
+contradiction.
+
+.. code-block:: idris
+
+    void : Void -> a
+
+Proving Theorems
+================
+
+When type checking dependent types, the type itself gets *normalised*.
+So imagine we want to prove the following theorem about the reduction
+behaviour of ``plus``:
+
+.. code-block:: idris
+
+    plusReduces : (n:Nat) -> plus Z n = n
+
+We’ve written down the statement of the theorem as a type, in just the
+same way as we would write the type of a program. In fact there is no
+real distinction between proofs and programs. A proof, as far as we are
+concerned here, is merely a program with a precise enough type to
+guarantee a particular property of interest.
+
+We won’t go into details here, but the Curry-Howard correspondence [#Timothy]_
+explains this relationship. The proof itself is immediate, because
+``plus Z n`` normalises to ``n`` by the definition of ``plus``:
+
+.. code-block:: idris
+
+    plusReduces n = Refl
+
+It is slightly harder if we try the arguments the other way, because
+plus is defined by recursion on its first argument. The proof also works
+by recursion on the first argument to ``plus``, namely ``n``.
+
+.. code-block:: idris
+
+    plusReducesZ : (n:Nat) -> n = plus n Z
+    plusReducesZ Z = Refl
+    plusReducesZ (S k) = cong S (plusReducesZ k)
+
+``cong`` is a function defined in the library which states that equality
+respects function application:
+
+.. code-block:: idris
+
+    cong : (f : t -> u) -> a = b -> f a = f b
+
+To see more detail on what's going on, we can replace the recursive call to
+``plusReducesZ`` with a hole:
+
+.. code-block:: idris
+    
+    plusReducesZ (S k) = cong S ?help
+
+Then inspecting the type of the hole at the REPL shows us:
+
+::
+
+    Main> :t help
+       k : Nat
+    -------------------------------------
+    help : k = (plus k Z)
+
+We can do the same for the reduction behaviour of plus on successors:
+
+.. code-block:: idris
+
+    plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
+    plusReducesS Z m = Refl
+    plusReducesS (S k) m = cong S (plusReducesS k m)
+
+Even for small theorems like these, the proofs are a little tricky to
+construct in one go. When things get even slightly more complicated, it
+becomes too much to think about to construct proofs in this “batch
+mode”.
+
+Idris provides interactive editing capabilities, which can help with
+building proofs. For more details on building proofs interactively in
+an editor, see :ref:`proofs-index`.
+
+.. _sect-parity:
+
+Theorems in Practice
+====================
+
+The need to prove theorems can arise naturally in practice. For example,
+previously (:ref:`sec-views`) we implemented ``natToBin`` using a function
+``parity``:
+
+.. code-block:: idris
+
+    parity : (n:Nat) -> Parity n
+
+We provided a definition for ``parity``, but without explanation.  We might
+have hoped that it would look something like the following:
+
+.. code-block:: idris
+
+    parity : (n:Nat) -> Parity n
+    parity Z     = Even {n=Z}
+    parity (S Z) = Odd {n=Z}
+    parity (S (S k)) with (parity k)
+      parity (S (S (j + j)))     | Even = Even {n=S j}
+      parity (S (S (S (j + j)))) | Odd  = Odd {n=S j}
+
+Unfortunately, this fails with a type error:
+
+::
+
+    With.idr:26:17--27:3:While processing right hand side of Main.with block in 2419 at With.idr:24:3--27:3:
+    Can't solve constraint between:
+            plus j (S j)
+    and
+            S (plus j j)
+
+The problem is that normalising ``S j + S j``, in the type of ``Even``
+doesn't result in what we need for the type of the right hand side of
+``Parity``. We know that ``S (S (plus j j))`` is going to be equal to
+``S j + S j``, but we need to explain it to Idris with a proof. We can
+begin by adding some *holes* (see :ref:`sect-holes`) to the definition:
+
+.. code-block:: idris
+
+    parity : (n:Nat) -> Parity n
+    parity Z     = Even {n=Z}
+    parity (S Z) = Odd {n=Z}
+    parity (S (S k)) with (parity k)
+      parity (S (S (j + j)))     | Even = let result = Even {n=S j} in
+                                              ?helpEven
+      parity (S (S (S (j + j)))) | Odd  = let result = Odd {n=S j} in
+                                              ?helpOdd
+
+Checking the type of ``helpEven`` shows us what we need to prove for the
+``Even`` case:
+
+::
+
+      j : Nat
+      result : Parity (S (plus j (S j)))
+    --------------------------------------
+    helpEven : Parity (S (S (plus j j)))
+
+We can therefore write a helper function to *rewrite* the type to the form
+we need:
+
+.. code-block:: idris
+
+    helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
+    helpEven j p = rewrite plusSuccRightSucc j j in p
+
+The ``rewrite ... in`` syntax allows you to change the required type of an
+expression by rewriting it according to an equality proof. Here, we have
+used ``plusSuccRightSucc``, which has the following type:
+
+.. code-block:: idris
+
+    plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right
+
+We can see the effect of ``rewrite`` by replacing the right hand side of
+``helpEven`` with a hole, and working step by step. Beginning with the following:
+
+.. code-block:: idris
+
+    helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
+    helpEven j p = ?helpEven_rhs
+
+We can look at the type of ``helpEven_rhs``:
+
+.. code-block:: idris
+
+      j : Nat
+      p : Parity (S (plus j (S j)))
+    --------------------------------------
+    helpEven_rhs : Parity (S (S (plus j j)))
+
+Then we can ``rewrite`` by applying ``plusSuccRightSucc j j``, which gives
+an equation ``S (j + j) = j + S j``, thus replacing ``S (j + j)`` (or,
+in this case, ``S (plus j j)`` since ``S (j + j)`` reduces to that) in the
+type with ``j + S j``:
+
+.. code-block:: idris
+
+    helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
+    helpEven j p = rewrite plusSuccRightSucc j j in ?helpEven_rhs
+
+Checking the type of ``helpEven_rhs`` now shows what has happened, including
+the type of the equation we just used (as the type of ``_rewrite_rule``):
+
+.. code-block:: idris
+
+    Main> :t helpEven_rhs
+       j : Nat
+       p : Parity (S (plus j (S j)))
+    -------------------------------------
+    helpEven_rhs : Parity (S (plus j (S j)))
+
+Using ``rewrite`` and another helper for the ``Odd`` case, we can complete
+``parity`` as follows:
+
+.. code-block:: idris
+
+    helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
+    helpEven j p = rewrite plusSuccRightSucc j j in p
+
+    helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
+    helpOdd j p = rewrite plusSuccRightSucc j j in p
+
+    parity : (n:Nat) -> Parity n
+    parity Z     = Even {n=Z}
+    parity (S Z) = Odd {n=Z}
+    parity (S (S k)) with (parity k)
+      parity (S (S (j + j)))     | Even = helpEven j (Even {n = S j})
+      parity (S (S (S (j + j)))) | Odd  = helpOdd j (Odd {n = S j})
+
+Full details of ``rewrite`` are beyond the scope of this introductory tutorial,
+but it is covered in the theorem proving tutorial (see :ref:`proofs-index`).
+
+.. _sect-totality:
+
+Totality Checking
+=================
+
+If we really want to trust our proofs, it is important that they are
+defined by *total* functions — that is, a function which is defined for
+all possible inputs and is guaranteed to terminate. Otherwise we could
+construct an element of the empty type, from which we could prove
+anything:
+
+.. code-block:: idris
+
+    -- making use of 'hd' being partially defined
+    empty1 : Void
+    empty1 = hd [] where
+        hd : List a -> a
+        hd (x :: xs) = x
+
+    -- not terminating
+    empty2 : Void
+    empty2 = empty2
+
+Internally, Idris checks every definition for totality, and we can check at
+the prompt with the ``:total`` command. We see that neither of the above
+definitions is total:
+
+::
+
+    Void> :total empty1
+    Void.empty1 is not covering due to call to function empty1:hd
+    Void> :total empty2
+    Void.empty2 is possibly not terminating due to recursive path Void.empty2
+
+Note the use of the word “possibly” — a totality check can never be certain due
+to the undecidability of the halting problem. The check is, therefore,
+conservative. It is also possible (and indeed advisable, in the case of proofs)
+to mark functions as total so that it will be a compile time error for the
+totality check to fail:
+
+.. code-block:: idris
+
+    total empty2 : Void
+    empty2 = empty2
+
+Reassuringly, our proof in Section :ref:`sect-empty` that the zero and
+successor constructors are disjoint is total:
+
+.. code-block:: idris
+
+    Main> :total disjoint
+    Main.disjoint is Total
+
+The totality check is, necessarily, conservative. To be recorded as
+total, a function ``f`` must:
+
+-  Cover all possible inputs
+
+-  Be *well-founded* — i.e. by the time a sequence of (possibly
+   mutually) recursive calls reaches ``f`` again, it must be possible to
+   show that one of its arguments has decreased.
+
+-  Not use any data types which are not *strictly positive*
+
+-  Not call any non-total functions
+
+Directives and Compiler Flags for Totality
+------------------------------------------
+
+[NOTE: Not all of this is implemented yet for Idris 2]
+
+By default, Idris allows all well-typed definitions, whether total or not.
+However, it is desirable for functions to be total as far as possible, as this
+provides a guarantee that they provide a result for all possible inputs, in
+finite time. It is possible to make total functions a requirement, either:
+
+-  By using the ``--total`` compiler flag.
+
+-  By adding a ``%default total`` directive to a source file. All
+   definitions after this will be required to be total, unless
+   explicitly flagged as ``partial``.
+
+All functions *after* a ``%default total`` declaration are required to
+be total. Correspondingly, after a ``%default partial`` declaration, the
+requirement is relaxed.
+
+Finally, the compiler flag ``--warnpartial`` causes to print a warning
+for any undeclared partial function.
+
+Totality checking issues
+------------------------
+
+Please note that the totality checker is not perfect! Firstly, it is
+necessarily conservative due to the undecidability of the halting
+problem, so many programs which *are* total will not be detected as
+such. Secondly, the current implementation has had limited effort put
+into it so far, so there may still be cases where it believes a function
+is total which is not. Do not rely on it for your proofs yet!
+
+Hints for totality
+------------------
+
+In cases where you believe a program is total, but Idris does not agree, it is
+possible to give hints to the checker to give more detail for a termination
+argument. The checker works by ensuring that all chains of recursive calls
+eventually lead to one of the arguments decreasing towards a base case, but
+sometimes this is hard to spot. For example, the following definition cannot be
+checked as ``total`` because the checker cannot decide that ``filter (< x) xs``
+will always be smaller than ``(x :: xs)``:
+
+.. code-block:: idris
+
+    qsort : Ord a => List a -> List a
+    qsort [] = []
+    qsort (x :: xs)
+       = qsort (filter (< x) xs) ++
+          (x :: qsort (filter (>= x) xs))
+
+The function ``assert_smaller``, defined in the prelude, is intended to
+address this problem:
+
+.. code-block:: idris
+
+    assert_smaller : a -> a -> a
+    assert_smaller x y = y
+
+It simply evaluates to its second argument, but also asserts to the
+totality checker that ``y`` is structurally smaller than ``x``. This can
+be used to explain the reasoning for totality if the checker cannot work
+it out itself. The above example can now be written as:
+
+.. code-block:: idris
+
+    total
+    qsort : Ord a => List a -> List a
+    qsort [] = []
+    qsort (x :: xs)
+       = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
+          (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))
+
+The expression ``assert_smaller (x :: xs) (filter (<= x) xs)`` asserts
+that the result of the filter will always be smaller than the pattern
+``(x :: xs)``.
+
+In more extreme cases, the function ``assert_total`` marks a
+subexpression as always being total:
+
+.. code-block:: idris
+
+    assert_total : a -> a
+    assert_total x = x
+
+In general, this function should be avoided, but it can be very useful
+when reasoning about primitives or externally defined functions (for
+example from a C library) where totality can be shown by an external
+argument.
+
+
+.. [#Timothy] Timothy G. Griffin. 1989. A formulae-as-type notion of
+       control. In Proceedings of the 17th ACM SIGPLAN-SIGACT
+       symposium on Principles of programming languages (POPL
+       '90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714
+       http://doi.acm.org/10.1145/96709.96714

docs/source/tutorial/views.rst

@@ -0,0 +1,156 @@
+.. _sec-views:
+
+*****************************
+Views and the “``with``” rule
+*****************************
+
+[NOT UPDATED FOR IDRIS 2 YET]
+
+Dependent pattern matching
+==========================
+
+Since types can depend on values, the form of some arguments can be
+determined by the value of others. For example, if we were to write
+down the implicit length arguments to ``(++)``, we’d see that the form
+of the length argument was determined by whether the vector was empty
+or not:
+
+.. code-block:: idris
+
+    (++) : Vect n a -> Vect m a -> Vect (n + m) a
+    (++) {n=Z}   []        ys = ys
+    (++) {n=S k} (x :: xs) ys = x :: xs ++ ys
+
+If ``n`` was a successor in the ``[]`` case, or zero in the ``::``
+case, the definition would not be well typed.
+
+.. _sect-nattobin:
+
+The ``with`` rule — matching intermediate values
+================================================
+
+Very often, we need to match on the result of an intermediate
+computation. Idris provides a construct for this, the ``with``
+rule, inspired by views in ``Epigram`` [#McBridgeMcKinna]_, which takes account of
+the fact that matching on a value in a dependently typed language can
+affect what we know about the forms of other values. In its simplest
+form, the ``with`` rule adds another argument to the function being
+defined.
+
+We have already seen a vector filter function. This time, we define it
+using ``with`` as follows:
+
+.. code-block:: idris
+
+    filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
+    filter p [] = ( _ ** [] )
+    filter p (x :: xs) with (filter p xs)
+      filter p (x :: xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
+
+Here, the ``with`` clause allows us to deconstruct the result of
+``filter p xs``. The view refined argument pattern ``filter p (x ::
+xs)`` goes beneath the ``with`` clause, followed by a vertical bar
+``|``, followed by the deconstructed intermediate result ``( _ ** xs'
+)``. If the view refined argument pattern is unchanged from the
+original function argument pattern, then the left side of ``|`` is
+extraneous and may be omitted:
+
+.. code-block:: idris
+
+    filter p (x :: xs) with (filter p xs)
+      | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
+
+``with`` clauses can also be nested:
+
+.. code-block:: idris
+
+    foo : Int -> Int -> Bool
+    foo n m with (n + 1)
+      foo _ m | 2 with (m + 1)
+        foo _ _ | 2 | 3 = True
+        foo _ _ | 2 | _ = False
+      foo _ _ | _ = False
+
+If the intermediate computation itself has a dependent type, then the
+result can affect the forms of other arguments — we can learn the form
+of one value by testing another. In these cases, view refined argument
+patterns must be explicit. For example, a ``Nat`` is either even or
+odd. If it is even it will be the sum of two equal ``Nat``.
+Otherwise, it is the sum of two equal ``Nat`` plus one:
+
+.. code-block:: idris
+
+    data Parity : Nat -> Type where
+       Even : {n : _} -> Parity (n + n)
+       Odd  : {n : _} -> Parity (S (n + n))
+
+We say ``Parity`` is a *view* of ``Nat``. It has a *covering function*
+which tests whether it is even or odd and constructs the predicate
+accordingly. Note that we're going to need access to ``n`` at run time, so
+although it's an implicit argument, it has unrestricted multiplicity.
+
+.. code-block:: idris
+
+    parity : (n:Nat) -> Parity n
+
+We’ll come back to the definition of ``parity`` shortly. We can use it
+to write a function which converts a natural number to a list of
+binary digits (least significant first) as follows, using the ``with``
+rule:
+
+.. code-block:: idris
+
+    natToBin : Nat -> List Bool
+    natToBin Z = Nil
+    natToBin k with (parity k)
+       natToBin (j + j)     | Even = False :: natToBin j
+       natToBin (S (j + j)) | Odd  = True  :: natToBin j
+
+The value 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 ``|``, we also write how the results affect the other
+patterns left of the ``|``. That is:
+
+- When ``parity k`` evaluates to ``Even``, we can refine the original
+  argument ``k`` to a refined pattern ``(j + j)`` according to
+  ``Parity (n + n)`` from the ``Even`` constructor definition. So
+  ``(j + j)`` replaces ``k`` on the left side of ``|``, and the
+  ``Even`` constructor appears on the right side. The natural number
+  ``j`` in the refined pattern can be used on the right side of the
+  ``=`` sign.
+
+- Otherwise, when ``parity k`` evaluates to ``Odd``, the original
+  argument ``k`` is refined to ``S (j + j)`` according to ``Parity (S
+  (n + n))`` from the ``Odd`` constructor definition, and ``Odd`` now
+  appears on the right side of ``|``, again with the natural number
+  ``j`` used on the right side of the ``=`` sign.
+
+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.
+
+Defining ``parity``
+===================
+
+The definition of ``parity`` is a little tricky, and requires some knowledge of
+theorem proving (see Section :ref:`sect-theorems`), but for completeness, here
+it is:
+
+.. code-block:: idris
+
+    parity : (n : Nat) -> Parity n
+    parity Z = Even {n = Z}
+    parity (S Z) = Odd {n = Z}
+    parity (S (S k)) with (parity k)
+      parity (S (S (j + j))) | Even
+          = rewrite plusSuccRightSucc j j in Even {n = S j}
+      parity (S (S (S (j + j)))) | Odd
+          = rewrite plusSuccRightSucc j j in Odd {n = S j}
+
+For full details on ``rewrite`` in particular, please refer to the theorem
+proving tutorial, in Section :ref:`proofs-index`.
+
+.. [#McBridgeMcKinna] Conor McBride and James McKinna. 2004. The view from the
+       left. J. Funct. Program. 14, 1 (January 2004),
+       69-111. https://doi.org/10.1017/S0956796803004829

docs/source/typedd/typedd.rst

@@ -0,0 +1,456 @@
+.. _typedd-index:
+
+Type Driven Development with Idris: Updates Required
+====================================================
+
+The code in the book `Type-Driven Development with Idris
+<https://www.manning.com/books/type-driven-development-with-idris>`_ by Edwin
+Brady, available from `Manning <https://www.manning.com>`_,  will mostly work
+in Idris 2, with some small changes as detailed in this document. The updated
+code is also [going to be] part of the test suite (see `tests/typedd-book
+<https://github.com/edwinb/Idris2/tree/master/tests/typedd-book>`_ in the Idris
+2 source).
+
+If you are new to Idris, and learning from the book, we recommend working
+through the first 3-4 chapters with Idris 1, to avoid the need to worry about
+the changes described here. After that, refer to this document for any
+necessary changes.
+
+Chapter 1
+---------
+
+No changes necessary
+
+Chapter 2
+---------
+
+The Prelude is smaller than Idris 1, and many functions have been moved to
+the base libraries instead. So:
+
+In ``Average.idr``, add:
+
+.. code-block:: idris
+
+    import Data.Strings -- for `words`
+    import Data.List -- for `length` on lists
+
+In ``AveMain.idr`` and ``Reverse.idr`` add:
+
+.. code-block:: idris
+
+    import System.REPL -- for 'repl'
+
+Chapter 3
+---------
+
+Unbound implicits have multiplicity 0, so we can't match on them at run-time.
+Therefore, in ``Matrix.idr``, we need to change the type of ``createEmpties``
+and ``transposeMat`` so that the length of the inner vector is available to
+match on:
+
+.. code-block:: idris
+
+    createEmpties : {n : _} -> Vect n (Vect 0 elem)
+    transposeMat : {n : _} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
+
+Chapter 4
+---------
+
+For the reasons described above:
+
++ In ``DataStore.idr``, add ``import System.REPL`` and ``import Data.Strings``
++ In ``SumInputs.idr``, add ``import System.REPL``
++ In ``TryIndex.idr``, add an implicit argument:
+
+.. code-block:: idris
+
+    tryIndex : {n : _} -> Integer -> Vect n a -> Maybe a
+
+Chapter 5
+---------
+
+There is no longer a ``Cast`` instance from ``String`` to ``Nat``, because its
+behaviour of returing Z if the ``String`` wasn't numeric was thought to be
+confusing and potentially error prone. Instead, there is ``stringToNatOrZ`` in
+``Data.Strings`` which at least has a clearer name. So:
+
+In ``Loops.idr`` and ``ReadNum.idr`` add ``import Data.Strings`` and change ``cast`` to
+``stringToNatOrZ``
+
+Chapter 6
+---------
+
+In ``DataStore.idr`` and ``DataStoreHoles.idr``, add ``import Data.Strings`` and
+``import System.REPL``. Also in ``DataStore.idr``, the ``schema`` argument to
+``display`` is required for matching, so change the type to:
+
+.. code-block:: idris
+
+    display : {schema : _} -> SchemaType schema -> String
+
+In ``TypeFuns.idr`` add ``import Data.Strings``
+
+Chapter 7
+---------
+
+``Abs`` is now a separate interface from ``Neg``. So, change the type of ``eval``
+to include ``Abs`` specifically:
+
+.. code-block:: idris
+
+    eval : (Abs num, Neg num, Integral num) => Expr num -> num
+
+Also, take ``abs`` out of the ``Neg`` implementation for ``Expr`` and add an
+implementation of ``Abs`` as follows:
+
+.. code-block:: idris
+
+    Abs ty => Abs (Expr ty) where
+        abs = Abs
+
+Chapter 8
+---------
+
+In ``AppendVec.idr``, add ``import Data.Nat`` for the ``Nat`` proofs
+
+``cong`` now takes an explicit argument for the function to apply. So, in
+``CheckEqMaybe.idr`` change the last case to:
+
+.. code-block:: idris
+
+    checkEqNat (S k) (S j) = case checkEqNat k j of
+                                  Nothing => Nothing
+                                  Just prf => Just (cong S prf)
+
+A similar change is necessary in ``CheckEqDec.idr``.
+
+In ``ExactLength.idr``, the ``m`` argument to ``exactLength`` is needed at run time,
+so change its type to:
+
+.. code-block:: idris
+
+    exactLength : {m : _} ->
+                  (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
+
+A similar change is necessary in ``ExactLengthDec.idr``. Also, ``DecEq`` is no
+longer part of the prelude, so add ``import Decidable.Equality``.
+
+In ``ReverseVec.idr``, add ``import Data.Nat`` for the ``Nat`` proofs.
+
+Chapter 9
+---------
+
++ In ``ElemType.idr``, add ``import Decidable.Equality``
+
+In ``Hangman.idr``:
+
++ Add ``import Decidable.Equality`` and ``import Data.Strings``
++ ``removeElem`` pattern matches on ``n``, so it needs to be written in its
+  type:
+
+.. code-block:: idris
+
+    removeElem : {n : _} ->
+                 (value : a) -> (xs : Vect (S n) a) ->
+                 {auto prf : Elem value xs} ->
+                 Vect n a
+
++ ``letters`` is used by ``processGuess``, because it's passed to ``removeElem``:
+
+.. code-block:: idris
+
+    processGuess : {letters : _} ->
+                   (letter : Char) -> WordState (S guesses) (S letters) ->
+                   Either (WordState guesses (S letters))
+                          (WordState (S guesses) letters)
+
++ ``guesses`` and ``letters`` are implicit arguments to ``game``, but are used by the
+  definition, so add them to its type:
+
+.. code-block:: idris
+
+    game : {guesses : _} -> {letters : _} ->
+           WordState (S guesses) (S letters) -> IO Finished
+
+In ``RemoveElem.idr``
+
++ ``removeElem`` needs to be updated as above.
+
+Chapter 10
+----------
+
+Lots of changes necessary here, at least when constructing views, due to Idris
+2 having a better (that is, more precise and correct!) implementation of
+unification, and the rules for recursive ``with`` application being tightened up.
+
+In ``MergeSort.idr``, add ``import Data.List``
+
+In ``MergeSortView.idr``, add ``import Data.List``, and make the arguments to the
+views explicit:
+
+.. code-block:: idris
+
+    mergeSort : Ord a => List a -> List a
+    mergeSort input with (splitRec input)
+      mergeSort [] | SplitRecNil = []
+      mergeSort [x] | SplitRecOne x = [x]
+      mergeSort (lefts ++ rights) | (SplitRecPair lefts rights lrec rrec)
+           = merge (mergeSort lefts | lrec)
+                   (mergeSort rights | rrec)
+
+In ``SnocList.idr``, in ``my_reverse``, the link between ``Snoc rec`` and ``xs ++ [x]``
+needs to be made explicit. Idris 1 would happily decide that ``xs`` and ``x`` were
+the relevant implicit arguments to ``Snoc`` but this was little more than a guess
+based on what would make it type check, whereas Idris 2 is more precise in
+what it allows to unify. So, ``x`` and ``xs`` need to be explicit arguments to
+``Snoc``:
+
+.. code-block:: idris
+
+    data SnocList : List a -> Type where
+         Empty : SnocList []
+         Snoc : (x, xs : _) -> (rec : SnocList xs) -> SnocList (xs ++ [x])
+
+Correspondingly, they need to be explicit when matching. For example:
+
+.. code-block:: idris
+
+      my_reverse : List a -> List a
+      my_reverse input with (snocList input)
+        my_reverse [] | Empty = []
+        my_reverse (xs ++ [x]) | (Snoc x xs rec) = x :: my_reverse xs | rec
+
+Similar changes are necessary in ``snocListHelp`` and ``my_reverse_help``. See
+tests/typedd-book/chapter10/SnocList.idr for the full details.
+
+Also, in ``snocListHelp``, ``input`` is used at run time so needs to be bound
+in the type:
+
+.. code-block:: idris
+
+    snocListHelp : {input : _} ->
+                   (snoc : SnocList input) -> (rest : List a) -> SnocList (input +
+
+It's no longer necessary to give ``{input}`` explicitly in the patterns for
+``snocListHelp``, although it's harmless to do so.
+
+In ``IsSuffix.idr``, the matching has to be written slightly differently. The
+recursive with application in Idris 1 probably shouldn't have allowed this!
+
+.. code-block:: idris
+
+    isSuffix : Eq a => List a -> List a -> Bool
+    isSuffix input1 input2 with (snocList input1, snocList input2)
+      isSuffix [] input2 | (Empty, s) = True
+      isSuffix input1 [] | (s, Empty) = False
+      isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec, Snoc ysrec)
+         = if x == y
+              then isSuffix xs ys | (xsrec, ysrec)
+              else False
+
+This doesn't yet get past the totality checker, however, because it doesn't
+know about looking inside pairs.
+
+In ``DataStore.idr``: Well this is embarrassing - I've no idea how Idris 1 lets
+this through! I think perhaps it's too "helpful" when solving unification
+problems. To fix it, add an extra parameter ``schema`` to ``StoreView``, and change
+the type of ``SNil`` to be explicit that the ``empty`` is the function defined in
+``DataStore``. Also add ``entry`` and ``store`` as explicit arguments to ``SAdd``:
+
+.. code-block:: idris
+
+    data StoreView : (schema : _) -> DataStore schema -> Type where
+         SNil : StoreView schema DataStore.empty
+         SAdd : (entry, store : _) -> (rec : StoreView schema store) ->
+                StoreView schema (addToStore entry store)
+
+Since ``size`` is as explicit argument in the ``DataStore`` record, it also needs
+to be relevant in the type of ``storeViewHelp``:
+
+.. code-block:: idris
+
+    storeViewHelp : {size : _} ->
+                    (items : Vect size (SchemaType schema)) ->
+                    StoreView schema (MkData size items)
+
+In ``TestStore.idr``:
+
++ In ``listItems``, ``empty`` needs to be ``DataStore.empty`` to be explicit that you
+  mean the function
++ In ``filterKeys``, there is an error in the ``SNil`` case, which wasn't caught
+  because of the type of ``SNil`` above. It should be:
+
+.. code-block:: idris
+
+      filterKeys test DataStore.empty | SNil = []
+
+Chapter 11
+----------
+
+In ``Streams.idr`` add ``import Data.Stream`` for ``iterate``.
+
+In ``Arith.idr`` and ``ArithTotal.idr``, the ``Divides`` view now has explicit
+arguments for the dividend and remainder, so they need to be explicit in
+``bound``:
+
+.. code-block:: idris
+
+    bound : Int -> Int
+    bound x with (divides x 12)
+      bound ((12 * div) + rem) | (DivBy div rem prf) = rem + 1
+
+In ``ArithCmd.idr``, update ``DivBy`` as above. Also add ``import Data.Strings`` for
+``Strings.toLower``.
+
+In ``ArithCmd.idr``, update ``DivBy`` and ``import Data.Strings`` as above. Also,
+since export rules are per-namespace now, rather than per-file, you need to
+export ``(>>=)`` from the namespaces ``CommandDo`` and ``ConsoleDo``.
+
+Chapter 12
+----------
+
+For reasons described above: In ``ArithState.idr``, add ``import Data.Strings``.
+Also the ``(>>=)`` operators need to be set as ``export`` since they are in their
+own namespaces, and in ``getRandom``, ``DivBy`` needs to take additional
+arguments ``div`` and ``rem``.
+
+Chapter 13
+----------
+
+In ``StackIO.idr``:
+
++ ``tryAdd`` pattern matches on ``height``, so it needs to be written in its
+  type:
+
+.. code-block:: idris
+
+    tryAdd : {height : _} -> StackIO height
+
++ ``height`` is also an implicit argument to ``stackCalc``, but is used by the
+  definition, so add it to its type:
+
+.. code-block:: idris
+
+    stackCalc : {height : _} -> StackIO height
+
++ In ``StackDo`` namespace, export ``(>>=)``:
+
+.. code-block:: idris
+
+    namespace StackDo
+      export
+      (>>=) : StackCmd a height1 height2 ->
+              (a -> Inf (StackIO height2)) -> StackIO height1
+              (>>=) = Do
+
+In ``Vending.idr``:
+
++ Add ``import Data.Strings`` and change ``cast`` to ``stringToNatOrZ`` in ``strToInput``
++ In ``MachineCmd`` type, add an implicit argument to ``(>>=)`` data constructor:
+
+.. code-block:: idris
+
+    (>>=) : {state2 : _} ->
+            MachineCmd a state1 state2 ->
+            (a -> MachineCmd b state2 state3) ->
+            MachineCmd b state1 state3
+
++ In ``MachineIO`` type, add an implicit argument to ``Do`` data constructor:
+
+.. code-block:: idris
+
+    data MachineIO : VendState -> Type where
+      Do : {state1 : _} ->
+           MachineCmd a state1 state2 ->
+           (a -> Inf (MachineIO state2)) -> MachineIO state1
+
++ ``runMachine`` pattern matches on ``inState``, so it needs to be written in its
+  type:
+
+.. code-block:: idris
+
+    runMachine : {inState : _} -> MachineCmd ty inState outState -> IO ty
+
++ In ``MachineDo`` namespace, add an implicit argument to ``(>>=)`` and export it:
+
+.. code-block:: idris
+
+    namespace MachineDo
+      export
+      (>>=) : {state1 : _} ->
+              MachineCmd a state1 state2 ->
+              (a -> Inf (MachineIO state2)) -> MachineIO state1
+      (>>=) = Do
+
++ ``vend`` and ``refill`` pattern match on ``pounds`` and ``chocs``, so they need to be written in
+  their type:
+
+.. code-block:: idris
+
+    vend : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs)
+    refill: {pounds : _} -> {chocs : _} -> (num : Nat) -> MachineIO (pounds, chocs)
+
++ ``pounds`` and ``chocs`` are implicit arguments to ``machineLoop``, but are used by the
+  definition, so add them to its type:
+
+.. code-block:: idris
+
+    machineLoop : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs)
+
+Chapter 14
+----------
+
+In ``ATM.idr``:
+
++ Add ``import Data.Strings`` and change ``cast`` to ``stringToNatOrZ`` in ``runATM``
+
+In ``ATM.idr``, add:
+
+.. code-block:: idris
+
+    import Data.Strings -- for `toUpper`
+    import Data.List -- for `nub`
+
++ In ``Loop`` namespace, export ``GameLoop`` type and its data constructors:
+
+.. code-block:: idris
+
+    namespace Loop
+      public export
+      data GameLoop : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
+        (>>=) : GameCmd a state1 state2_fn ->
+                ((res : a) -> Inf (GameLoop b (state2_fn res) state3_fn)) ->
+                GameLoop b state1 state3_fn
+        Exit : GameLoop () NotRunning (const NotRunning)
+
++ ``letters`` and ``guesses`` are used by ``gameLoop``, so they need to be written in its type:
+
+.. code-block:: idris
+
+    gameLoop : {letters : _} -> {guesses : _} ->
+               GameLoop () (Running (S guesses) (S letters)) (const NotRunning)
+
++ In ``Game`` type, add an implicit argument ``letters`` to ``InProgress`` data constructor:
+
+.. code-block:: idris
+
+    data Game : GameState -> Type where
+      GameStart : Game NotRunning
+      GameWon : (word : String) -> Game NotRunning
+      GameLost : (word : String) -> Game NotRunning
+      InProgress : {letters : _} -> (word : String) -> (guesses : Nat) ->
+                   (missing : Vect letters Char) -> Game (Running guesses letters)
+
++ ``removeElem`` pattern matches on ``n``, so it needs to be written in its type:
+
+.. code-block:: idris
+
+    removeElem : {n : _} ->
+                 (value : a) -> (xs : Vect (S n) a) ->
+                 {auto prf : Elem value xs} ->
+                 Vect n a
+
+Chapter 15
+----------
+
+TODO

docs/source/updates/updates.rst

@@ -0,0 +1,659 @@
+.. _updates-index:
+
+#####################
+Changes since Idris 1
+#####################
+
+Idris 2 is mostly backwards compatible with Idris 1, with some minor
+exceptions. This document describes the changes, approximately in order of
+likelihood of encountering them in practice. New features are described at
+the end, in Section :ref:`sect-new-features`.
+
+The Section :ref:`typedd-index` describes how these changes affect the code
+in the book `Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_
+by Edwin Brady, available from `Manning <https://www.manning.com>`_.
+
+.. note::
+   The documentation for Idris has been published under the Creative
+   Commons CC0 License. As such to the extent possible under law, *The
+   Idris Community* has waived all copyright and related or neighboring
+   rights to Documentation for Idris.
+
+   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+
+New Core Language: Quantities in Types
+======================================
+
+Idris 2 is based on `Quantitative Type Theory (QTT)
+<https://bentnib.org/quantitative-type-theory.html>`_, a core language
+developed by Bob Atkey and Conor McBride. In practice, this means that every
+variable in Idris 2 has a *quantity* associated with it. A quantity is one of:
+
+* ``0``, meaning that the variable is *erased* at run time
+* ``1``, meaning that the variable is used *exactly once* at run time
+* *Unrestricted*, which is the same behaviour as Idris 1
+
+For more details on this, see Section :ref:`sect-multiplicities`. In practice,
+this might cause some Idris 1 programs not to type check in Idris 2 due to
+attempting to use an argument which is erased at run time.
+
+Erasure
+-------
+
+In Idris, names which begin with a lower case later are automatically bound
+as implicit arguments in types, for example in the following skeleton
+definition, ``n``, ``a`` and ``m`` are implicitly bound:
+
+.. code-block:: idris
+
+    append : Vect n a -> Vect m a -> Vect (n + m) a
+    append xs ys = ?append_rhs
+
+One of the difficulties in compiling a dependently typed programming language
+is deciding which arguments are used at run time and which can safely be
+erased. More importantly, it's one of the difficulties when programming: how
+can a programmer *know* when an argument will be erased?
+
+In Idris 2, a variable's quantity tells us whether it will be available at
+run time or not. We can see the quantities of the variables in scope in
+``append_rhs`` by inspecting the hole at the REPL:
+
+::
+
+    Main> :t append_rhs
+     0 m : Nat
+     0 a : Type
+     0 n : Nat
+       ys : Vect m a
+       xs : Vect n a
+    -------------------------------------
+    append_rhs : Vect (plus n m) a
+
+The ``0`` next to ``m``, ``a`` and ``n`` mean that they are in scope, but there
+will be ``0`` occurrences at run-time. That is, it is *guaranteed* that they
+will be erased at run-time.
+
+This does lead to some potential difficulties when converting Idris 1 programs,
+if you are using implicit arguments at run time.  For example, in Idris 1 you
+can get the length of a vector as follows:
+
+.. code-block:: idris
+
+    vlen : Vect n a -> Nat
+    vlen {n} xs = n
+
+This might seem like a good idea, since it runs in constant time and takes
+advantage of the type level information, but the trade off is that ``n`` has to
+be available at run time, so at run time we always need the length of the
+vector to be available if we ever call ``vlen``. Idris 1 can infer whether the
+length is needed, but there's no easy way for a programmer to be sure.
+
+In Idris 2, we need to state explicitly that ``n`` is needed at run time
+
+.. code-block:: idris
+
+    vlen : {n : Nat} -> Vect n a -> Nat
+    vlen xs = n
+
+(Incidentally, also note that in Idris 2, names bound in types are also available
+in the definition without explicitly rebinding them.)
+
+This also means that when you call ``vlen``, you need the length available. For
+example, this will give an error
+
+.. code-block:: idris
+
+    sumLengths : Vect m a -> Vect n a —> Nat
+    sumLengths xs ys = vlen xs + vlen ys
+
+Idris 2 reports::
+
+  vlen.idr:7:20--7:28:While processing right hand side of Main.sumLengths at vlen.idr:7:1--10:1:
+  m is not accessible in this context
+
+This means that it needs to use ``m`` as an argument to pass to ``vlen xs``,
+where it needs to be available at run time, but ``m`` is not available in
+``sumLengths`` because it has multiplicity ``0``.
+
+We can see this more clearly by replacing the right hand side of
+``sumLengths`` with a hole...
+
+.. code-block:: idris
+
+    sumLengths : Vect m a -> Vect n a -> Nat
+    sumLengths xs ys = ?sumLengths_rhs
+
+...then checking the hole's type at the REPL::
+
+  Main> :t sumLengths_rhs
+   0 n : Nat
+   0 a : Type
+   0 m : Nat
+     ys : Vect n a
+     xs : Vect m a
+  -------------------------------------
+  sumLengths_rhs : Nat
+
+Instead, we need to give bindings for ``m`` and ``n`` with
+unrestricted multiplicity
+
+.. code-block:: idris
+
+    sumLengths : {m, n : _} -> Vect m a -> Vect n a —> Nat
+    sumLengths xs ys = vLen xs + vLen xs
+
+Remember that giving no multiplicity on a binder, as with ``m`` and ``n`` here,
+means that the variable has unrestricted usage.
+
+If you're converting Idris 1 programs to work with Idris 2, this is probably the
+biggest thing you need to think about. It is important to note,
+though, that if you have bound implicits, such as...
+
+.. code-block:: idris
+
+    excitingFn : {t : _} -> Coffee t -> Moonbase t
+
+...then it's a good idea to make sure ``t`` really is needed, or performance
+might suffer due to the run time building the instance of ``t`` unnecessarily!
+
+One final note on erasure: it is an error to try to pattern match on an
+argument with multiplicity ``0``, unless its value is inferrable from
+elsewhere. So, the following definition is rejected
+
+.. code-block:: idris
+
+    badNot : (0 x : Bool) -> Bool
+    badNot False = True
+    badNot True = False
+
+This is rejected with the error::
+
+  badnot.idr:2:1--3:1:Attempt to match on erased argument False in
+  Main.badNot
+
+The following, however, is fine, because in ``sNot``, even though we appear
+to match on the erased argument ``x``, its value is uniquely inferrable from
+the type of the second argument
+
+.. code-block:: idris
+
+    data SBool : Bool -> Type where
+         SFalse : SBool False
+         STrue  : SBool True
+
+    sNot : (0 x : Bool) -> SBool x -> Bool
+    sNot False SFalse = True
+    sNot True  STrue  = False
+
+Experience with Idris 2 so far suggests that, most of the time, as long as
+you're using unbound implicits in your Idris 1 programs, they will work without
+much modification in Idris 2. The Idris 2 type checker will point out where you
+require an unbound implicit argument at run time - sometimes this is both
+surprising and enlightening!
+
+
+Linearity
+---------
+
+Full details on linear arguments with multiplicity ``1`` are given in Section
+:ref:`sect-multiplicities`. In brief, the intuition behind multiplicity ``1`` is
+that if we have a function with a type of the following form...
+
+.. code-block:: idris
+
+    f : (1 x : a) -> b
+
+...then the guarantee given by the type system is that *if* ``f x`` *is used
+exactly once, then* ``x`` *is used exactly once* in the process.
+
+Prelude and ``base`` libraries
+==============================
+
+The Prelude in Idris 1 contained a lot of definitions, many of them rarely
+necessary. The philosophy in Idris 2 is different. The (rather vaguely
+specified) rule of thumb is that it should contain the basic functions
+required by almost any non-trivial program.
+
+This is a vague specification since different programmers will consider
+different things absolutely necessary, but the result is that it contains:
+
+- Anything the elaborator can desugar to (e.g. tuples, ``()``, ``=``)
+- Basic types ``Bool``, ``Nat``, ``List``, ``Stream``, ``Dec``, ``Maybe``,
+  ``Either``
+- The most important utility functions: ``id``, ``the``, composition, etc
+- Interfaces for arithmetic and implementations for the primitives and
+  basic types
+- Basic ``Char`` and ``String`` manipulation
+- ``Show``, ``Eq``, ``Ord``, and implementations for all types in the prelude
+- Interfaces and functions for basic proof (``cong``, ``Uninhabited``, etc)
+- ``Semigroup``, ``Monoid``
+- ``Functor``, ``Applicative``, ``Monad`` and related functions
+- ``Foldable``, ``Alternative`` and ``Traversable``
+- ``Enum``, for list range syntax
+- Console ``IO``
+
+Anything which doesn't fit in here has been moved to the ``base`` libraries.
+Among other places, you can find some of the functions which used to be
+in the prelude in:
+
+- ``Data.List`` and ``Data.Nat``
+- ``Data.Maybe`` and ``Data.Either``
+- ``System.File`` and ``System.Directory``, (file management was previously
+  part of the prelude)
+- ``Decidable.Equality``
+
+Smaller Changes
+===============
+
+Ambiguous Name Resolution
+-------------------------
+
+Idris 1 worked very hard to resolve ambiguous names, by type, even if this
+involved some complicated interaction with interface resolution. This could
+sometimes be the cause of long type checking times. Idris 2 simplifies this, at
+the cost of sometimes requiring more programmer annotations on ambiguous
+names.
+
+As a general rule, Idris 2 will be able to disambiguate between names which
+have different concrete return types (such as data constructors), or which have
+different concrete argument types (such as record projections). It may struggle
+to resolve ambiguities if one name requires an interface to be resolved.
+It will postpone resolution if a name can't be resolved immediately, but unlike
+Idris 1, it won't attempt significant backtracking. If you have deeply nested
+ambiguous names (beyond a small threshold, default 3) Idris 2 will report an
+error.  You can change this threshold with a directive, for example:
+
+.. code-block:: idris
+
+    %ambiguity_depth 10
+
+However, in such circumstances it is almost certainly a better idea to
+disambiguate explicitly.
+
+Indeed in general, if you get an ambiguous name error, the best approach is to
+give the namespace explicitly. You can also rebind names locally:
+
+.. code-block:: idris
+
+    Main> let (::) = Prelude.(::) in [1,2,3]
+    [1, 2, 3]
+
+One difficulty which remains is resolving ambiguous names where one possibility
+is an interface method, and another is a concrete top level function.
+For example, we may have:
+
+.. code-block:: idris
+
+    Prelude.(>>=) : Monad m => m a -> (a -> m b) -> m b
+    LinearIO.(>>=) : (1 act : IO a) -> (1 k : a -> IO b) -> IO b
+
+As a pragmatic choice, if type checking in a context where the more concrete
+name is valid (``LinearIO.(>>=)`` here, so if type checking an expression known
+to have type ``IO t`` for some ``t``), the more concrete name will be chosen.
+
+This is somehow unsatisfying, so we may revisit this in future!
+
+Modules, namespaces and export
+------------------------------
+
+The visibility rules, as controlled by the ``private``, ``export`` and
+``public export`` modifiers, now refer to the visibility of names from
+other *namespaces*, rather than other *files*.
+
+So if you have the following, all in the same file...
+
+.. code-block:: idris
+
+    namespace A
+      private
+      aHidden : Int -> Int
+      aHidden x = x * 2
+
+      export
+      aVisible : Int -> Int
+      aVisibile x = aHidden x
+
+    mamespace B
+      export
+      bVisible : Int -> Int
+      bVisible x = aVisible (x * 2)
+
+...then ``bVisible`` can access ``aVisible``, but not ``aHidden``.
+
+Records are, as before, defined in their own namespace, but fields are always
+visible from the parent namespace.
+
+Also, module names must now match the filename in which they're defined, with
+the exception of the module ``Main``, which can be defined in a file with
+any name.
+
+``%language`` pragmas
+---------------------
+
+There are several ``%language`` pragmas in Idris 1, which define various
+experimental extensions. None of these are available in Idris 2, although
+extensions may be defined in the future.
+
+``let`` bindings
+----------------
+
+``let`` bindings, i.e. expressions of the form ``let x = val in e`` have
+slightly different behaviour. Previously, you could rely on the computational
+behaviour of ``x`` in the scope of ``e``, so type checking could take into
+account that ``x`` reduces to ``val``. Unfortunately, this leads to complications
+with ``case`` and ``with`` clauses: if we want to preserve the computational
+behaviour, we would need to make significant changes to the way ``case`` and
+``with`` are elaborated.
+
+So, for simplicity and consistency (and, realistically, because I don't have
+enough time to resolve the problem for ``case`` and ``with``) the above
+expression ``let x = val in e`` is equivalent to ``(\x => e) val``.
+
+So, ``let`` now effectively generalises a complex subexpression.
+If you do need the computational behaviour of a definition, it is now possible
+using local function definitions instead - see Section :ref:`sect-local-defs`
+below.
+
+``auto``-implicits and Interfaces
+---------------------------------
+
+Interfaces and ``auto``-implicit arguments are similar, in that they invoke an
+expression search mechanism to find the value of an argument. In Idris 1,
+they were implemented separately, but in Idris 2, they use the same mechanism.
+Consider the following *total* definition of ``fromMaybe``:
+
+.. code-block:: idris
+
+    data IsJust : Maybe a -> Type where
+         ItIsJust : IsJust (Just val)
+
+    fromMaybe : (x : Maybe a) -> {auto p : IsJust x} -> a
+    fromMaybe (Just x) {p = ItIsJust} = x
+
+Since interface resolution and ``auto``-implicits are now the same thing,
+the type of ``fromMaybe`` can be written as:
+
+.. code-block:: idris
+
+    fromMaybe : (x : Maybe a) -> IsJust x => a
+
+So now, the constraint arrow ``=>`` means that the argument will be found
+by ``auto``-implicit search.
+
+When defining a ``data`` type, there are ways to control how ``auto``-implicit
+search will proceed, by giving options to the data type. For example:
+
+.. code-block:: idris
+
+    data Elem : (x : a) -> (xs : List a) -> Type where
+         [search x]
+         Here : Elem x (x :: xs)
+         There : Elem x xs -> Elem x (y :: xs)
+
+The ``search x`` option means that ``auto``-implicit search for a value of
+type ``Elem t ts`` will start as soon as the type checker has resolved the
+value ``t``, even if ``ts`` is still unknown.
+
+By default, ``auto``-implicit search uses the constructors of a data type
+as search hints. The ``noHints`` option on a data type turns this behaviour
+off.
+
+You can add your own search hints with the ``%hint`` option on a function.
+For example:
+
+.. code-block:: idris
+
+    data MyShow : Type -> Type where
+         [noHints]
+         MkMyShow : (myshow : a -> String) -> MyShow a
+
+    %hint
+    showBool : MyShow Bool
+    showBool = MkMyShow (\x => if x then "True" else "False")
+
+    myShow : MyShow a => a -> String
+    myShow @{MkMyShow myshow} = myshow
+
+In this case, searching for ``MyShow Bool`` will find ``showBool``, as we
+can see if we try evaluating ``myShow True`` at the REPL:
+
+::
+
+    Main> myShow True
+    "True"
+
+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!
+
+Totality and Coverage
+---------------------
+
+``%default covering`` is now the default status [Actually still TODO, but
+planned soon!]
+
+Build artefacts
+---------------
+
+This is not really a language change, but a change in the way Idris saves
+checked files, and still useful to know. All checked modules are now saved in a
+directory ``build/ttc``, in the root of the source tree, with the directory
+structure following the directory structure of the source.  Executables are
+placed in ``build/exec``.
+
+.. _sect-new-features:
+
+New features
+============
+
+As well as the change to the core language to use quantitative type theory,
+described above, there are several other new features.
+
+.. _sect-local-defs:
+
+Local function definitions
+--------------------------
+
+Functions can now be defined locally, using a ``let`` block. For example,
+``greet`` in the following example, which is defined in the scope of a local
+variable ``x``:
+
+.. code-block:: idris
+
+    chat : IO ()
+    chat
+        = do putStr "Name: "
+             x <- getLine
+             let greet : String -> String
+                 greet msg = msg ++ " " ++ x
+             putStrLn (greet "Hello")
+             putStrLn (greet "Bye")
+
+These ``let`` blocks can be used anywhere (in the middle of ``do`` blocks
+as above, but also in any function, or in type declarations).
+``where`` blocks are now elaborated by translation into a local ``let``.
+
+However, Idris no longer attempts to infer types for functions defined in
+``where`` blocks, because this was fragile. This may be reinstated, if we can
+come up with a good, predictable approach.
+
+Scope of implicit arguments
+---------------------------
+
+Implicit arguments in a type are now in scope in the body of a definition.
+We've already seen this above, where ``n`` is in scope automatically in the
+body of ``vlen``:
+
+.. code-block:: idris
+
+    vlen : {n : Nat} -> Vect n a -> Nat
+    vlen xs = n
+
+This is important to remember when using ``where`` blocks, or local definitions,
+since the names in scope will also be in scope when declaring the *type* of
+the local definition. For example, the following definition, where we attempt
+to define our own version of ``Show`` for ``Vect``, will fail to type check:
+
+.. code-block:: idris
+
+    showVect : Show a => Vect n a -> String
+    showVect xs = "[" ++ showBody xs ++ "]"
+      where
+        showBody : Vect n a -> String
+        showBody [] = ""
+        showBody [x] = show x
+        showBody (x :: xs) = show x ++ ", " ++ showBody xs
+
+This fails because ``n`` is in scope already, from the type of ``showVect``,
+in the type declaration for ``showBody``, and so the first clause ``showBody
+[]`` will fail to type check because ``[]`` has length ``Z``, not ``n``. We can
+fix this by locally binding ``n``:
+
+.. code-block:: idris
+
+    showVect : Show a => Vect n a -> String
+    showVect xs = "[" ++ showBody xs ++ "]"
+      where
+        showBody : forall n . Vect n a -> String
+        ...
+
+Or, alternatively, using a new name:
+
+.. code-block:: idris
+
+    showVect : Show a => Vect n a -> String
+    showVect xs = "[" ++ showBody xs ++ "]"
+      where
+        showBody : Vect n' a -> String
+        ...
+
+Idris 1 took a different approach here: names which were parameters to data
+types were in scope, other names were not. The Idris 2 approach is, we hope,
+more consistent and easier to understand.
+
+Better inference
+----------------
+
+In Idris 1, holes (that is, unification variables arising from implicit
+arguments) were local to an expression, and if they were not resolved while
+checking the expression, they would not be resolved at all. In Idris 2,
+they are global, so inference works better. For example, we can now say:
+
+.. code-block:: idris
+
+    test : Vect ? Int
+    test = [1,2,3,4]
+
+    Main> :t test
+    Main.test : Vect (S (S (S (S Z)))) Int
+
+The ``?``, incidentally, differs from ``_`` in that ``_`` will be bound as
+an implicit argument if unresolved after checking the type of ``test``, but
+``?`` will be left as a hole to be resolved later. Otherwise, they can be
+used interchangeably.
+
+Dependent case
+--------------
+
+``case`` blocks were available in Idris 1, but with some restrictions. Having
+better inference means that ``case`` blocks work more effectively in Idris 2,
+and dependent case analysis is supported.
+
+.. code-block:: idris
+
+    append : Vect n a -> Vect m a -> Vect (n + m) a
+    append xs ys
+        = case xs of
+               [] => ys
+               (x :: xs) => x :: append xs ys
+
+The implicit arguments and original values are still available in the body of
+the ``case``. Somewhat contrived, but the following is valid:
+
+.. code-block:: idris
+
+    info : {n : _} -> Vect n a -> (Vect n a, Nat)
+    info xs
+        = case xs of
+               [] => (xs, n)
+               (y :: ys) => (xs, n)
+
+
+Record updates
+--------------
+
+Dependent record updates work, provided that all relevant fields are updated
+at the same time. Dependent record update is implemented via dependent ``case``
+blocks rather than by generating a specific update function for each field as
+in Idris 1, so you will no longer get mystifying errors when trying to update
+dependent records!
+
+For example, we can wrap a vector in a record, with an explicit length
+field:
+
+.. code-block:: idris
+
+    record WrapVect a where
+      constructor MkVect
+      purpose : String
+      length : Nat
+      content : Vect length a
+
+Then, we can safely update the ``content``, provided we update the ``length``
+correspondingly:
+
+.. code-block:: idris
+
+    addEntry : String -> WrapVect String -> WrapVect String
+    addEntry val = record { length $= S,
+                            content $= (val :: ) }
+
+Generate definition
+-------------------
+
+A new feature of the IDE protocol supports generating complete definitions from
+a type signature. You can try this at the REPL, for example, given our
+favourite introductory example...
+
+.. code-block:: idris
+
+    append : Vect n a -> Vect m a -> Vect (n + m) a
+
+...assuming this is defined on line 3, you can use the ``:gd`` command as
+follows:
+
+.. code-block:: idris
+
+    Main> :gd 3 append
+    append [] ys = ys
+    append (x :: xs) ys = x :: append xs ys
+
+This works by a fairly simple brute force search, which tries searching for a
+valid right hand side, and case splitting on the left if that fails, but is
+remarkably effective in a lot of situations. Some other examples which work:
+
+.. code-block:: idris
+
+    my_cong : forall f . (x : a) -> (y : a) -> x = y -> f x = f y
+    my_curry : ((a, b) -> c) -> a -> b -> c
+    my_uncurry : (a -> b -> c) -> (a, b) -> c
+    append : Vect n a -> Vect m a -> Vect (n + m) a
+    lappend : (1 xs : List a) -> (1 ys : List a) -> List a
+    zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
+
+This is available in the IDE protocol via the ``generate-def`` command.
+
+Chez Scheme target
+------------------
+
+The default code generator is, for the moment, `Chez Scheme
+<https://www.scheme.com/>`_. A Racket code generator is also available. There
+is not yet a way to plug in code generators as in Idris 1, but this is coming.
+To change the code generator, you can use the ``:set cg`` command:
+
+::
+
+    Main> :set cg racket
+
+Early experience shows that both are much faster than the Idris 1 C code
+generator, in both compile time and execution time (but we haven't done any
+formal study on this yet, so it's just anecdotal evidence).