diff options
Diffstat (limited to 'doc/sphinx/preamble.rst')
-rw-r--r-- | doc/sphinx/preamble.rst | 92 |
1 files changed, 92 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}} + \] |