[ doc ] with-abstraction

agda · Nov 5, 2015 · b93e320 · b93e320
1 parent a0f7210
commit b93e320
Show file tree

Hide file tree

Showing 9 changed files with 655 additions and 5 deletions.
diff --git a/doc/user-manual/conf.py b/doc/user-manual/conf.py
@@ -30,7 +30,8 @@
 # Add any Sphinx extension module names here, as strings. They can be
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
 # ones.
-extensions = []
+extensions = ['sphinx.ext.pngmath']
+pngmath_use_preview = True
 
 # Add any paths that contain templates here, relative to this directory.
 templates_path = ['_templates']

diff --git a/doc/user-manual/language/built-ins.rst b/doc/user-manual/language/built-ins.rst
@@ -4,6 +4,10 @@
 Built-ins
 *********
 
+.. contents::
+   :depth: 1
+   :local:
+
 The Agda type checker knows about, and has special treatment for, a number of
 different concepts. The most prominent is natural numbers, which has a special
 representation as Haskell integers and support for fast arithmetic. The surface
@@ -275,6 +279,8 @@ available on strings (given suitable bindings for `Bool <Booleans_>`_, `Char
 
 String literals can be :ref:`overloaded <overloaded-strings>`.
 
+.. _built-in-equality:
+
 Equality
 --------
 

diff --git a/doc/user-manual/language/core-language.rst b/doc/user-manual/language/core-language.rst
@@ -0,0 +1,24 @@
+.. _core-language:
+
+*************
+Core language
+*************
+
+.. note::
+   This is a stub
+
+.. code-block:: haskell
+
+  data Term = Var Int Elims
+            | Def QName Elims               -- ^ @f es@, possibly a delta/iota-redex
+            | Con ConHead Args              -- ^ @c vs@
+            | Lam ArgInfo (Abs Term)        -- ^ Terms are beta normal. Relevance is ignored
+            | Lit Literal
+            | Pi (Dom Type) (Abs Type)      -- ^ dependent or non-dependent function space
+            | Sort Sort
+            | Level Level
+            | MetaV MetaId Elims
+            | DontCare Term
+              -- ^ Irrelevant stuff in relevant position, but created
+              --   in an irrelevant context.
+
diff --git a/doc/user-manual/language/function-definitions.rst b/doc/user-manual/language/function-definitions.rst
@@ -6,3 +6,11 @@ Function Definitions
 
 .. note::
    This is a stub.
+
+Pattern matching
+----------------
+
+.. _dot-patterns:
+
+Dot patterns
+~~~~~~~~~~~~
diff --git a/doc/user-manual/language/index.rst b/doc/user-manual/language/index.rst
@@ -10,6 +10,7 @@ Language Reference
    built-ins
    coinduction
    copatterns
+   core-language
    data-types
    foreign-function-interface
    function-definitions

diff --git a/doc/user-manual/language/lambda-abstraction.rst b/doc/user-manual/language/lambda-abstraction.rst
@@ -6,3 +6,8 @@ Lambda Abstraction
 
 .. note::
    This is a stub.
+
+.. _pattern-lambda:
+
+Pattern matching lambda
+-----------------------
diff --git a/doc/user-manual/language/module-system.rst b/doc/user-manual/language/module-system.rst
@@ -6,3 +6,8 @@ Module System
 
 .. note::
    This is a stub.
+
+.. _anonymous-modules:
+
+Anonymous modules
+-----------------
diff --git a/doc/user-manual/language/termination-checking.rst b/doc/user-manual/language/termination-checking.rst
@@ -6,3 +6,8 @@ Termination Checking
 
 .. note::
    This is a stub.
+
+.. _termination-checking-with:
+
+With-functions
+--------------