diff options
author | 2018-03-11 00:02:02 +0100 | |
---|---|---|
committer | 2018-03-12 09:58:57 +0100 | |
commit | b97c80a39bb3471ae681fe5f5afef8a973e4c606 (patch) | |
tree | ef7a24ad672f72018dbee0cbb9d99727288cba97 /doc | |
parent | 16b4db7d5d5ee64c09d02db6305799673d7efa80 (diff) |
[Sphinx] Add doc preamble
Diffstat (limited to 'doc')
-rw-r--r-- | doc/sphinx/preamble.rst | 92 | ||||
-rw-r--r-- | doc/sphinx/replaces.rst | 78 |
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`` |