[ user manual ] language reference skeleton

I pulled the topics off the old reference manual on the wiki and added what I could think of. There are sure to be things missing (not to mention there's nothing in the files yet).
agda · Oct 13, 2015 · fe5ec8c · fe5ec8c
1 parent 2fa477a
commit fe5ec8c
Show file tree

Hide file tree

Showing 40 changed files with 340 additions and 8 deletions.
diff --git a/doc/user-manual/getting-started.rst b/doc/user-manual/getting-started.rst
@@ -0,0 +1,8 @@
+.. _getting-started:
+
+*****
+Getting Started
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/index.rst b/doc/user-manual/index.rst
@@ -6,14 +6,14 @@
 Welcome to Agda's documentation!
 ================================
 
-Contents:
-
 .. toctree::
    :maxdepth: 2
 
+   overview
+   getting-started
+   language/index
+   tools/index
    license
-   compilers
-   reflection
 
 
 Indices and tables

diff --git a/doc/user-manual/language/built-ins.rst b/doc/user-manual/language/built-ins.rst
@@ -0,0 +1,8 @@
+.. _built-ins:
+
+*****
+Built-ins
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/coinduction.rst b/doc/user-manual/language/coinduction.rst
@@ -0,0 +1,8 @@
+.. _coinduction:
+
+*****
+Coinduction
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/copatterns.rst b/doc/user-manual/language/copatterns.rst
@@ -0,0 +1,8 @@
+.. _copatterns:
+
+*****
+Copatterns
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/data-types.rst b/doc/user-manual/language/data-types.rst
@@ -0,0 +1,8 @@
+.. _data-types:
+
+*****
+Data Types
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/foreign-function-interface.rst b/doc/user-manual/language/foreign-function-interface.rst
@@ -0,0 +1,8 @@
+.. _foreign-function-interface:
+
+*****
+Foreign Function Interface
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/function-definitions.rst b/doc/user-manual/language/function-definitions.rst
@@ -0,0 +1,8 @@
+.. _function-definitions:
+
+*****
+Function Definitions
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/function-types.rst b/doc/user-manual/language/function-types.rst
@@ -0,0 +1,8 @@
+.. _function-types:
+
+*****
+Function Types
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/implicit-arguments.rst b/doc/user-manual/language/implicit-arguments.rst
@@ -0,0 +1,8 @@
+.. _implicit-arguments:
+
+*****
+Implicit Arguments
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/index.rst b/doc/user-manual/language/index.rst
@@ -0,0 +1,39 @@
+.. _language-index:
+
+##################
+Language Reference
+##################
+
+.. toctree::
+   :maxdepth: 2
+
+   built-ins
+   coinduction
+   copatterns
+   data-types
+   foreign-function-interface
+   function-definitions
+   function-types
+   implicit-arguments
+   instance-arguments
+   irrelevance
+   lambda-abstraction
+   let-expressions
+   lexical-structure
+   literal-overloading
+   mixfix-operators
+   module-system
+   mutual-recursion
+   pattern-synonyms
+   postulates
+   pragmas
+   record-types
+   reflection
+   safe-agda
+   sized-types
+   telescopes
+   termination-checking
+   universe-levels
+   with-abstraction
+   without-k
+
diff --git a/doc/user-manual/language/instance-arguments.rst b/doc/user-manual/language/instance-arguments.rst
@@ -0,0 +1,8 @@
+.. _instance-arguments:
+
+*****
+Instance Arguments
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/irrelevance.rst b/doc/user-manual/language/irrelevance.rst
@@ -0,0 +1,8 @@
+.. _irrelevance:
+
+*****
+Irrelevance
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/lambda-abstraction.rst b/doc/user-manual/language/lambda-abstraction.rst
@@ -0,0 +1,8 @@
+.. _lambda-abstraction:
+
+*****
+Lambda Abstraction
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/let-expressions.rst b/doc/user-manual/language/let-expressions.rst
@@ -0,0 +1,8 @@
+.. _let-expressions:
+
+*****
+Let Expressions
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/lexical-structure.rst b/doc/user-manual/language/lexical-structure.rst
@@ -0,0 +1,8 @@
+.. _lexical-structure:
+
+*****
+Lexical Structure
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/literal-overloading.rst b/doc/user-manual/language/literal-overloading.rst
@@ -0,0 +1,8 @@
+.. _literal-overloading:
+
+*****
+Literal Overloading
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/mixfix-operators.rst b/doc/user-manual/language/mixfix-operators.rst
@@ -0,0 +1,8 @@
+.. _mixfix-operators:
+
+*****
+Mixfix Operators
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/module-system.rst b/doc/user-manual/language/module-system.rst
@@ -0,0 +1,8 @@
+.. _module-system:
+
+*****
+Module System
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/mutual-recursion.rst b/doc/user-manual/language/mutual-recursion.rst
@@ -0,0 +1,8 @@
+.. _mutual-recursion:
+
+*****
+Mutual Recursion
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/pattern-synonyms.rst b/doc/user-manual/language/pattern-synonyms.rst
@@ -0,0 +1,8 @@
+.. _pattern-synonyms:
+
+*****
+Pattern Synonyms
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/postulates.rst b/doc/user-manual/language/postulates.rst
@@ -0,0 +1,8 @@
+.. _postulates:
+
+*****
+Postulates
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/pragmas.rst b/doc/user-manual/language/pragmas.rst
@@ -0,0 +1,8 @@
+.. _pragmas:
+
+*****
+Pragmas
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/record-types.rst b/doc/user-manual/language/record-types.rst
@@ -0,0 +1,8 @@
+.. _record-types:
+
+*****
+Record Types
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/reflection.rst → doc/user-manual/language/reflection.rst b/doc/user-manual/reflection.rst → doc/user-manual/language/reflection.rst
@@ -1,7 +1,8 @@
 .. _reflection:
 
+**********
 Reflection
-==========
+**********
 
 .. note::
    This section is not yet finished and may contain outdated material!

diff --git a/doc/user-manual/language/safe-agda.rst b/doc/user-manual/language/safe-agda.rst
@@ -0,0 +1,8 @@
+.. _safe-agda:
+
+*****
+Safe Agda
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/sized-types.rst b/doc/user-manual/language/sized-types.rst
@@ -0,0 +1,8 @@
+.. _sized-types:
+
+*****
+Sized Types
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/telescopes.rst b/doc/user-manual/language/telescopes.rst
@@ -0,0 +1,8 @@
+.. _telescopes:
+
+*****
+Telescopes
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/termination-checking.rst b/doc/user-manual/language/termination-checking.rst
@@ -0,0 +1,8 @@
+.. _termination-checking:
+
+*****
+Termination Checking
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/universe-levels.rst b/doc/user-manual/language/universe-levels.rst
@@ -0,0 +1,8 @@
+.. _universe-levels:
+
+*****
+Universe Levels
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/with-abstraction.rst b/doc/user-manual/language/with-abstraction.rst
@@ -0,0 +1,8 @@
+.. _with-abstraction:
+
+*****
+With Abstraction
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/language/without-k.rst b/doc/user-manual/language/without-k.rst
@@ -0,0 +1,8 @@
+.. _without-k:
+
+*****
+Without K
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/license.rst b/doc/user-manual/license.rst
@@ -1,7 +1,8 @@
 .. _License:
 
+################
 The Agda License
-================
+################
 
 Copyright (c) 2005-2015 Ulf Norell, Andreas Abel, Nils Anders
 Danielsson, Andrés Sicard-Ramírez, Dominique Devriese, Péter

diff --git a/doc/user-manual/overview.rst b/doc/user-manual/overview.rst
@@ -0,0 +1,8 @@
+.. _overview:
+
+********
+Overview
+********
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/compilers.rst → doc/user-manual/tools/compilers.rst b/doc/user-manual/compilers.rst → doc/user-manual/tools/compilers.rst
@@ -1,5 +1,8 @@
-Agda Compilers
-===================
+.. _compilers:
+
+***********
+Compilers
+***********
 
 Backends
 --------

diff --git a/doc/user-manual/tools/emacs-mode.rst b/doc/user-manual/tools/emacs-mode.rst
@@ -0,0 +1,8 @@
+.. _emacs-mode:
+
+*****
+Emacs Mode
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/tools/generating-html.rst b/doc/user-manual/tools/generating-html.rst
@@ -0,0 +1,8 @@
+.. _generating-html:
+
+*****
+Generating HTML
+*****
+
+.. note::
+   This is a stub.
diff --git a/doc/user-manual/tools/generating-latex.rst b/doc/user-manual/tools/generating-latex.rst
@@ -0,0 +1,8 @@
+.. _generating-latex:
+
+*****
+Generating LaTeX
+*****
+
+.. note::
+   This is a stub.