aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-11 00:02:02 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-12 09:58:57 +0100
commitb97c80a39bb3471ae681fe5f5afef8a973e4c606 (patch)
treeef7a24ad672f72018dbee0cbb9d99727288cba97 /doc
parent16b4db7d5d5ee64c09d02db6305799673d7efa80 (diff)
[Sphinx] Add doc preamble
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/preamble.rst92
-rw-r--r--doc/sphinx/replaces.rst78
2 files changed, 170 insertions, 0 deletions
diff --git a/doc/sphinx/preamble.rst b/doc/sphinx/preamble.rst
new file mode 100644
index 000000000..395f558a8
--- /dev/null
+++ b/doc/sphinx/preamble.rst
@@ -0,0 +1,92 @@
+.. preamble::
+
+ \[
+ \newcommand{\alors}{\textsf{then}}
+ \newcommand{\alter}{\textsf{alter}}
+ \newcommand{\as}{\kw{as}}
+ \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)}
+ \newcommand{\bool}{\textsf{bool}}
+ \newcommand{\case}{\kw{case}}
+ \newcommand{\conc}{\textsf{conc}}
+ \newcommand{\cons}{\textsf{cons}}
+ \newcommand{\consf}{\textsf{consf}}
+ \newcommand{\conshl}{\textsf{cons\_hl}}
+ \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)}
+ \newcommand{\emptyf}{\textsf{emptyf}}
+ \newcommand{\End}{\kw{End}}
+ \newcommand{\endkw}{\kw{end}}
+ \newcommand{\EqSt}{\textsf{EqSt}}
+ \newcommand{\even}{\textsf{even}}
+ \newcommand{\evenO}{\textsf{even_O}}
+ \newcommand{\evenS}{\textsf{even_S}}
+ \newcommand{\false}{\textsf{false}}
+ \newcommand{\filter}{\textsf{filter}}
+ \newcommand{\Fix}{\kw{Fix}}
+ \newcommand{\fix}{\kw{fix}}
+ \newcommand{\for}{\textsf{for}}
+ \newcommand{\forest}{\textsf{forest}}
+ \newcommand{\from}{\textsf{from}}
+ \newcommand{\Functor}{\kw{Functor}}
+ \newcommand{\haslength}{\textsf{has\_length}}
+ \newcommand{\hd}{\textsf{hd}}
+ \newcommand{\ident}{\textsf{ident}}
+ \newcommand{\In}{\kw{in}}
+ \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)}
+ \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)}
+ \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)}
+ \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}}
+ \newcommand{\injective}{\kw{injective}}
+ \newcommand{\kw}[1]{\textsf{#1}}
+ \newcommand{\lb}{\lambda}
+ \newcommand{\length}{\textsf{length}}
+ \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3}
+ \newcommand{\List}{\textsf{list}}
+ \newcommand{\lra}{\longrightarrow}
+ \newcommand{\Match}{\kw{match}}
+ \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})}
+ \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})}
+ \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})}
+ \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})}
+ \newcommand{\mto}{.\;}
+ \newcommand{\Nat}{\mathbb{N}}
+ \newcommand{\nat}{\textsf{nat}}
+ \newcommand{\Nil}{\textsf{nil}}
+ \newcommand{\nilhl}{\textsf{nil\_hl}}
+ \newcommand{\nO}{\textsf{O}}
+ \newcommand{\node}{\textsf{node}}
+ \newcommand{\nS}{\textsf{S}}
+ \newcommand{\odd}{\textsf{odd}}
+ \newcommand{\oddS}{\textsf{odd_S}}
+ \newcommand{\ovl}[1]{\overline{#1}}
+ \newcommand{\Pair}{\textsf{pair}}
+ \newcommand{\Prod}{\textsf{prod}}
+ \newcommand{\Prop}{\textsf{Prop}}
+ \newcommand{\return}{\kw{return}}
+ \newcommand{\Set}{\textsf{Set}}
+ \newcommand{\si}{\textsf{if}}
+ \newcommand{\sinon}{\textsf{else}}
+ \newcommand{\Sort}{\cal S}
+ \newcommand{\Str}{\textsf{Stream}}
+ \newcommand{\Struct}{\kw{Struct}}
+ \newcommand{\subst}[3]{#1\{#2/#3\}}
+ \newcommand{\tl}{\textsf{tl}}
+ \newcommand{\tree}{\textsf{tree}}
+ \newcommand{\true}{\textsf{true}}
+ \newcommand{\Type}{\textsf{Type}}
+ \newcommand{\unfold}{\textsf{unfold}}
+ \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}}
+ \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}}
+ \newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]}
+ \newcommand{\WFE}[1]{\WF{E}{#1}}
+ \newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)}
+ \newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}
+ \newcommand{\with}{\kw{with}}
+ \newcommand{\WS}[3]{#1[] \vdash #2 <: #3}
+ \newcommand{\WSE}[2]{\WS{E}{#1}{#2}}
+ \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4}
+ \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
+ \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}}
+ \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}}
+ \newcommand{\zeroone}[1]{[{#1}]}
+ \newcommand{\zeros}{\textsf{zeros}}
+ \]
diff --git a/doc/sphinx/replaces.rst b/doc/sphinx/replaces.rst
new file mode 100644
index 000000000..2c38219b9
--- /dev/null
+++ b/doc/sphinx/replaces.rst
@@ -0,0 +1,78 @@
+.. some handy replacements for common items
+
+.. role:: smallcaps
+
+.. |A_1| replace:: `A`\ :math:`_{1}`
+.. |A_n| replace:: `A`\ :math:`_{n}`
+.. |arg_1| replace:: `arg`\ :math:`_{1}`
+.. |arg_n| replace:: `arg`\ :math:`_{n}`
+.. |bdi| replace:: :math:`\beta\delta\iota`
+.. |binder_1| replace:: `binder`\ :math:`_{1}`
+.. |binder_n| replace:: `binder`\ :math:`_{n}`
+.. |binders_1| replace:: `binders`\ :math:`_{1}`
+.. |binders_n| replace:: `binders`\ :math:`_{n}`
+.. |C_1| replace:: `C`\ :math:`_{1}`
+.. |c_1| replace:: `c`\ :math:`_{1}`
+.. |C_2| replace:: `C`\ :math:`_{2}`
+.. |c_i| replace:: `c`\ :math:`_{i}`
+.. |c_n| replace:: `c`\ :math:`_{n}`
+.. |Cic| replace:: :smallcaps:`Cic`
+.. |class_1| replace:: `class`\ :math:`_{1}`
+.. |class_2| replace:: `class`\ :math:`_{2}`
+.. |Coq| replace:: :smallcaps:`Coq`
+.. |CoqIDE| replace:: :smallcaps:`CoqIDE`
+.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\small{\beta\delta\iota\zeta}}`
+.. |Gallina| replace:: :smallcaps:`Gallina`
+.. |ident_0| replace:: `ident`\ :math:`_{0}`
+.. |ident_1,1| replace:: `ident`\ :math:`_{1,1}`
+.. |ident_1,k_1| replace:: `ident`\ :math:`_{1,k_1}`)
+.. |ident_1| replace:: `ident`\ :math:`_{1}`
+.. |ident_2| replace:: `ident`\ :math:`_{2}`
+.. |ident_3| replace:: `ident`\ :math:`_{3}`
+.. |ident_i| replace:: `ident`\ :math:`_{i}`
+.. |ident_j| replace:: `ident`\ :math:`_{j}`
+.. |ident_k| replace:: `ident`\ :math:`_{k}`
+.. |ident_n,1| replace:: `ident`\ :math:`_{n,1}`
+.. |ident_n,k_n| replace:: `ident`\ :math:`_{n,k_n}`
+.. |ident_n| replace:: `ident`\ :math:`_{n}`
+.. |L_tac| replace:: `L`:sub:`tac`
+.. |ML| replace:: :smallcaps:`ML`
+.. |mod_0| replace:: `mod`\ :math:`_{0}`
+.. |mod_1| replace:: `mod`\ :math:`_{1}`
+.. |mod_2| replace:: `mod`\ :math:`_{1}`
+.. |mod_n| replace:: `mod`\ :math:`_{n}`
+.. |module_0| replace:: `module`\ :math:`_{0}`
+.. |module_1| replace:: `module`\ :math:`_{1}`
+.. |module_expression_0| replace:: `module_expression`\ :math:`_{0}`
+.. |module_expression_1| replace:: `module_expression`\ :math:`_{1}`
+.. |module_expression_i| replace:: `module_expression`\ :math:`_{i}`
+.. |module_expression_n| replace:: `module_expression`\ :math:`_{n}`
+.. |module_n| replace:: `module`\ :math:`_{n}`
+.. |module_type_0| replace:: `module_type`\ :math:`_{0}`
+.. |module_type_1| replace:: `module_type`\ :math:`_{1}`
+.. |module_type_i| replace:: `module_type`\ :math:`_{i}`
+.. |module_type_n| replace:: `module_type`\ :math:`_{n}`
+.. |N| replace:: ``N``
+.. |nat| replace:: ``nat``
+.. |Ocaml| replace:: :smallcaps:`OCaml`
+.. |p_1| replace:: `p`\ :math:`_{1}`
+.. |p_i| replace:: `p`\ :math:`_{i}`
+.. |p_n| replace:: `p`\ :math:`_{n}`
+.. |Program| replace:: :strong:`Program`
+.. |t_1| replace:: `t`\ :math:`_{1}`
+.. |t_i| replace:: `t`\ :math:`_{i}`
+.. |t_m| replace:: `t`\ :math:`_{m}`
+.. |t_n| replace:: `t`\ :math:`_{n}`
+.. |term_0| replace:: `term`\ :math:`_{0}`
+.. |term_1| replace:: `term`\ :math:`_{1}`
+.. |term_2| replace:: `term`\ :math:`_{2}`
+.. |term_n| replace:: `term`\ :math:`_{n}`
+.. |type_0| replace:: `type`\ :math:`_{0}`
+.. |type_1| replace:: `type`\ :math:`_{1}`
+.. |type_2| replace:: `type`\ :math:`_{2}`
+.. |type_3| replace:: `type`\ :math:`_{3}`
+.. |type_n| replace:: `type`\ :math:`_{n}`
+.. |x_1| replace:: `x`\ :math:`_{1}`
+.. |x_i| replace:: `x`\ :math:`_{i}`
+.. |x_n| replace:: `x`\ :math:`_{n}`
+.. |Z| replace:: ``Z``