diff options
Diffstat (limited to 'doc/sphinx/refman-preamble.sty')
| -rw-r--r-- | doc/sphinx/refman-preamble.sty | 88 |
1 files changed, 88 insertions, 0 deletions
diff --git a/doc/sphinx/refman-preamble.sty b/doc/sphinx/refman-preamble.sty new file mode 100644 index 0000000000..b4fc608e47 --- /dev/null +++ b/doc/sphinx/refman-preamble.sty @@ -0,0 +1,88 @@ +\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{\kwend}{\kw{end}} +\newcommand{\EqSt}{\textsf{EqSt}} +\newcommand{\even}{\textsf{even}} +\newcommand{\evenO}{\textsf{even}_\textsf{O}} +\newcommand{\evenS}{\textsf{even}_\textsf{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}_\textsf{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}} |