diff --git a/docs/LICENSE b/docs/LICENSE
new file mode 100644
index 0000000..897ab8f
--- /dev/null
+++ b/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/
diff --git a/docs/Makefile b/docs/Makefile
new file mode 100644
index 0000000..d0c3cbf
--- /dev/null
+++ b/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)
diff --git a/docs/README.md b/docs/README.md
new file mode 100644
index 0000000..bb6d904
--- /dev/null
+++ b/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.
diff --git a/docs/make.bat b/docs/make.bat
new file mode 100644
index 0000000..6247f7e
--- /dev/null
+++ b/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
diff --git a/docs/source/app/index.rst b/docs/source/app/index.rst
new file mode 100644
index 0000000..190e7cc
--- /dev/null
+++ b/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...]
diff --git a/docs/source/backends/chez.rst b/docs/source/backends/chez.rst
new file mode 100644
index 0000000..dca0ce2
--- /dev/null
+++ b/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 `_. 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``.
diff --git a/docs/source/backends/index.rst b/docs/source/backends/index.rst
new file mode 100644
index 0000000..728a97a
--- /dev/null
+++ b/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 `_.
+
+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
+
diff --git a/docs/source/backends/racket.rst b/docs/source/backends/racket.rst
new file mode 100644
index 0000000..670c24b
--- /dev/null
+++ b/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]
diff --git a/docs/source/conf.py b/docs/source/conf.py
new file mode 100644
index 0000000..38d9e97
--- /dev/null
+++ b/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
diff --git a/docs/source/faq/faq.rst b/docs/source/faq/faq.rst
new file mode 100644
index 0000000..3c09075
--- /dev/null
+++ b/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.
diff --git a/docs/source/ffi/ffi.rst b/docs/source/ffi/ffi.rst
new file mode 100644
index 0000000..94d98a1
--- /dev/null
+++ b/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
+
+ 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
+
+ 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
diff --git a/docs/source/ffi/index.rst b/docs/source/ffi/index.rst
new file mode 100644
index 0000000..c82e86f
--- /dev/null
+++ b/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
diff --git a/docs/source/ffi/readline.rst b/docs/source/ffi/readline.rst
new file mode 100644
index 0000000..d9632f8
--- /dev/null
+++ b/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 `_ 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
+`_. 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 ``:
+
+::
+
+ 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 ()
diff --git a/docs/source/index.rst b/docs/source/index.rst
new file mode 100644
index 0000000..0b67fde
--- /dev/null
+++ b/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
diff --git a/docs/source/listing/idris-prompt-helloworld.txt b/docs/source/listing/idris-prompt-helloworld.txt
new file mode 100644
index 0000000..590c5cb
--- /dev/null
+++ b/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!
diff --git a/docs/source/listing/idris-prompt-interp.txt b/docs/source/listing/idris-prompt-interp.txt
new file mode 100644
index 0000000..69453ef
--- /dev/null
+++ b/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
diff --git a/docs/source/listing/idris-prompt-start.txt b/docs/source/listing/idris-prompt-start.txt
new file mode 100644
index 0000000..b3fb964
--- /dev/null
+++ b/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>
diff --git a/docs/source/proofs/definitional.rst b/docs/source/proofs/definitional.rst
new file mode 100644
index 0000000..f1229ee
--- /dev/null
+++ b/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.
diff --git a/docs/source/proofs/index.rst b/docs/source/proofs/index.rst
new file mode 100644
index 0000000..904c524
--- /dev/null
+++ b/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
diff --git a/docs/source/proofs/inductive.rst b/docs/source/proofs/inductive.rst
new file mode 100644
index 0000000..3618548
--- /dev/null
+++ b/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.
diff --git a/docs/source/proofs/patterns.rst b/docs/source/proofs/patterns.rst
new file mode 100644
index 0000000..bc18f33
--- /dev/null
+++ b/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.
diff --git a/docs/source/proofs/pluscomm.rst b/docs/source/proofs/pluscomm.rst
new file mode 100644
index 0000000..57a71e0
--- /dev/null
+++ b/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.
diff --git a/docs/source/proofs/propositional.rst b/docs/source/proofs/propositional.rst
new file mode 100644
index 0000000..0159b24
--- /dev/null
+++ b/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)
+
+
+
diff --git a/docs/source/reference/envvars.rst b/docs/source/reference/envvars.rst
new file mode 100644
index 0000000..a044b1d
--- /dev/null
+++ b/docs/source/reference/envvars.rst
@@ -0,0 +1,7 @@
+.. _ref-sect-envvars:
+
+*********************
+Environment Variables
+*********************
+
+[TODO: Fill in the environment variables recognised by Idris 2]
diff --git a/docs/source/reference/index.rst b/docs/source/reference/index.rst
new file mode 100644
index 0000000..273f6f1
--- /dev/null
+++ b/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
diff --git a/docs/source/reference/packages.rst b/docs/source/reference/packages.rst
new file mode 100644
index 0000000..1adece9
--- /dev/null
+++ b/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, `` = ``
+
+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 `_.
+
+Metadata
+--------
+
+The `iPKG` format supports additional metadata associated with the package.
+The added fields are:
+
++ ``brief = ""``, a string literal containing a brief description
+ of the package.
+
++ ``version = """``, a version string to associate with the package.
+
++ ``readme = """``, location of the README file.
+
++ ``license = ""``, a string description of the licensing
+ information.
+
++ ``authors = ""``, the author information.
+
++ ``maintainers = ""``, Maintainer information.
+
++ ``homepage = ""``, the website associated with the package.
+
++ ``sourceloc = ""``, the location of the DVCS where the source
+ can be found.
+
++ ``bugtracker = ""``, the location of the project's bug tracker.
+
+
+Common Fields
+-------------
+
+Other common fields which may be present in an ``ipkg`` file are:
+
++ ``executable =