setup.sty 12.2 KB
Newer Older
Giuseppe Castagna's avatar
Giuseppe Castagna committed
1
2
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{setup}[2018/04/25 v0.1]
3
4
\newcommand\hmmax{0}
\newcommand\bmmax{0}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
5
6
7
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Packages
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
8
\let\Bbbk\relax
Giuseppe Castagna's avatar
Giuseppe Castagna committed
9
%\usepackage{amsmath}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
10
\usepackage{mathtools}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
11
12
%\usepackage{amssymb}
%\usepackage{amsthm}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
13
\usepackage{alltt}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
14
\usepackage{bm}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
15
\usepackage{nicefrac}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
16
%\usepackage{stmaryrd}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
17
\usepackage{mathpartir}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
18
\usepackage{color}
Kim Nguyễn's avatar
Kim Nguyễn committed
19
\usepackage{listings}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
20
\usepackage[shortlabels]{enumitem}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
21
22

  
Giuseppe Castagna's avatar
Giuseppe Castagna committed
23
\definecolor{darkblue}{rgb}{0,0.2,0.4}
24
25
%\definecolor{darkred}{rgb}{0.7,0.4,0.4}
\definecolor{darkred}{rgb}{0.8,0.2,0.2}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
26

Giuseppe Castagna's avatar
Giuseppe Castagna committed
27
\ifwithcomments
28
\newcommand{\ignore}[1]{{\color{red}\textbf{DELETED:}#1}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
29
\newcommand{\beppe}[1]{{\bf\color{blue}Beppe: #1}}
30
\newcommand{\mick}[1]{{\bf\color{gray}Mickael: #1}}
Kim Nguyễn's avatar
Kim Nguyễn committed
31
\newcommand{\kim}[1]{{\bf\color{pink}Kim: #1}}
Victor Lanvin's avatar
Fixes    
Victor Lanvin committed
32
\newcommand{\victor}[1]{{\bf\color{purple}Victor: #1}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
33
34
35
36
37
\else
\newcommand{\ignore}[1]{}
\newcommand{\beppe}[1]{}
\newcommand{\mick}[1]{}
\newcommand{\kim}[1]{}
Victor Lanvin's avatar
Fixes    
Victor Lanvin committed
38
\newcommand{\victor}[1]{}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
39
\fi
Giuseppe Castagna's avatar
Giuseppe Castagna committed
40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Giuseppe Castagna's avatar
Giuseppe Castagna committed
41
42
43
44
45
46
47
48
49
50
51
% Style dependend definitions
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\ifelsevierstyle
\newcommand{\Appendix}{}
\else
\newcommand{\Appendix}{Appendix }
\fi
\newcommand{\svvspace}[1]{
  \iflongversion\else\vspace{#1}\fi
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Giuseppe Castagna's avatar
Giuseppe Castagna committed
52
53
54
55
56
57
58
59
% Support macros
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand {\DeclareMyOperator}[2] {%
  \expandafter\newcommand\csname#1\endcsname{\textsf{\textup{#2}}}}

\DeclareMathAlphabet {\MyMathBb} {U} {bbold} {m} {n}

Giuseppe Castagna's avatar
Giuseppe Castagna committed
60
61
62
63
64
65
66
67
68
69
70
71
72
73
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Inference rules
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def \TirNameStyle #1{\small #1}

\newcommand {\Infer} [4] [] {
  \inferrule*[%
    left={\ifx\\#1\\#1\else\ifx\\#2\\[\textsc{#1}]\:\else[\textsc{#1}]\fi\fi},%
    right={$ #4 $}%
  ]%
  {#2}{#3}}

\newcommand {\Rule}[1] {[\textsc{#1}]}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
74
\newcommand{\tcase}[4]{\ensuremath{(#1{\in}#2)\,\texttt{\textup{?}}\,#3\,\texttt{\textup{:}}\,#4}}
75
\newcommand{\letexp}[3]{\ensuremath{\texttt{\textup{let}}\,#1\,\texttt{\textup{=}}\,#2\,\texttt{\textup{in}}\,#3\,}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
76
\newcommand{\morecompact}{\baselineskip=9.5pt}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
77

Giuseppe Castagna's avatar
Giuseppe Castagna committed
78
79
80
81
82
83
\newcommand {\Pd} {\mathcal{P}}
\newcommand {\Pf} {\mathcal{P}_{\!\textup{fin}}}
\newcommand {\Domain} {\mathcal{D}}
\newcommand {\Constants} {\mathcal{C}}
\newcommand {\TypeInter}[1] {\llbracket #1 \rrbracket}
\def\dbar{{\mkern3mu\mathchar'26\mkern-7mu\raisebox{-.7pt}{$\mathchar'26$}\mkern-11mu d}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
84
\newcommand {\domega} {\partial} %possibilities: \dbar \dh \dj \delta
Giuseppe Castagna's avatar
Giuseppe Castagna committed
85
86
87
88
\newcommand {\Set}[1] {\{#1\}}
\newcommand {\ConstantsInBasicType} {\mathbb{B}}


Giuseppe Castagna's avatar
Giuseppe Castagna committed
89
90
\newcommand{\tauUp}{\tau^\Uparrow}
\newcommand{\sigmaUp}{\sigma^\Uparrow}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
91
\newcommand{\types}{\textbf{\textup{Types}}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
92
\newcommand{\occ}[2]{#1{\downarrow}#2}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
93
\newcommand{\basic}[1]{\text{\fontshape{\itdefault}\fontseries{\bfdefault}\selectfont b}_{#1}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
94
\newcommand{\tyof}[2]{\textsf{\textup{typeof}}_{#2}(#1)}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
95
\newcommand{\typof}[1]{\textsf{\textup{typeof}}(#1)}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
96
\newcommand{\typep}[3]{\textsf{\textup{Constr}}^{#1}_{#3}(#2)}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
97
\newcommand{\Gp}[2]{\textsf{Env}^{#1}_{#2}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
98
\newcommand{\ite}[4]{\ensuremath{\texttt{if}\;#1\in#2\;\texttt{then}\;#3\;\texttt{else}\;#4}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
99
\newcommand{\Let}[3]{\ensuremath{\texttt{let}\;#1\;\texttt{=}\;#2\;\texttt{in}\;#3}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
100
101
\newcommand{\anns}{\ensuremath{A}}
\newcommand{\ann}[2]{#1{\triangleright}#2}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
102
103
\newcommand{\alt}{~|~}
\newcommand{\arrow}[2]{#1\to #2}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
104
\newcommand{\pair}[2]{#1\times #2}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
105
\newcommand{\orecord}[1]{\pmb{\texttt{\{}}#1\ {\large\textbf{..}}\pmb{\texttt{\}}}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
106
107
\newcommand{\crecord}[1]{\pmb{\texttt{\{}}#1\pmb{\texttt{\}}}}
\newcommand{\erecord}[1]{\texttt{\{}#1\texttt{\}}}
Mickael Laurent's avatar
Mickael Laurent committed
108
\newcommand{\record}[2]{\{#1 ,\ \_ = #2\}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
109
110
111
112
113
114
115
116
117
118
119
120
\DeclareFontFamily{U}{mathb}{}
\DeclareFontShape{U}{mathb}{m}{n}{
  <-5.5> mathb5
  <5.5-6.5> mathb6
  <6.5-7.5> mathb7
  <7.5-8.5> mathb8
  <8.5-9.5> mathb9
  <9.5-11.5> mathb10
  <11.5-> mathb12
}{}
\DeclareSymbolFont{mathb}{U}{mathb}{m}{n}
\DeclareMathSymbol{\sqdot}{\mathbin}{mathb}{"0D}% name to be checked
121
\newcommand{\Cx}{\mathcal{C}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
122
\newcommand{\worra}[2]{#1\mathop{\,\sqdot\,} #2}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
123
\newcommand{\apply}[2]{#1\circ#2}
124
125
\newcommand {\Empty} {\ensuremath{\MyMathBb{0}}}
\newcommand {\Any} {\ensuremath{\MyMathBb{1}}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
126
\newcommand {\dom}[1]{\textsf{dom}(#1)}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
127
\newcommand {\Keyw} [1] {\text{\textsf{#1}}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
128
129
\newcommand {\False} {\Keyw{False}}
\newcommand {\True} {\Keyw{True}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
130
131
\newcommand {\Int} {\Keyw{Int}}
\newcommand {\Bool} {\Keyw{Bool}}
Kim Nguyễn's avatar
Kim Nguyễn committed
132
\newcommand {\Char} {\Keyw{Char}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
133
134
\newcommand {\Real} {\Keyw{Real}}
\newcommand {\Complex} {\Keyw{Complex}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
135
\newcommand {\String} {\Keyw{String}}
Mickael Laurent's avatar
Mickael Laurent committed
136
\newcommand{\Labels}{\Keyw{Labels}}
137
138
\newcommand{\Undef}{\Keyw{Undef}}
\newcommand{\undefcst}{\texttt{undef}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
139
\newcommand {\Cast}[2]{\tt #2\(\langle\)#1\(\rangle\)}
140
\newcommand {\MCast}[2]{#2\langle #1\rangle}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
141
\newcommand {\ifty}[4]{\ensuremath{\texttt{(}#1\in#2\texttt{)?}#3\texttt{:}#4}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
142
\newcommand {\code}[1]{\texttt{\color{darkblue}#1}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
143
\newcommand {\p}[1]{\texttt{#1}}
144
\newcommand {\iffdef}  {\hbox{\;\;$\iff$\hspace*{-5.94mm}\raise5pt\hbox{\rm\scriptsize def}\hspace*{4mm}}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
145
\newcommand {\eqdef}  {\hbox{\;\;$=$\hspace*{-2.94mm}\raise5pt\hbox{\rm\scriptsize def}\hspace*{1mm}}}
146
\newcommand {\eqdeftiny}  {\hbox{\;\;$=$\hspace*{-2.55mm}\raise5pt\hbox{\rm\tiny def}\hspace*{1.5mm}}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
147
148
149
\newcommand {\bpi} {\boldsymbol{\pi}}
\newcommand {\bpl}[1] {\boldsymbol{\pi}_{\boldsymbol 1}(#1)}
\newcommand {\bpr}[1] {\boldsymbol{\pi}_{\boldsymbol 2}(#1)}
150
\newcommand {\proj}[2] {#2.#1}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
151
\newcommand {\recupd}[3] {\texttt{\{} #1 \texttt{ with } #2 = #3 \texttt{\}}}
152
\newcommand {\recdel}[2] {#1 \mathtt{ \setminus } #2}
153
\DeclareMathOperator{\eqq}{\texttt{=?}}
154
155
156
157
158
159
160
161
162
163
164
165
166
167

% ---------------------------------------------------------------------------------

% New packages
\usepackage{bbm}

% New commands
\DeclarePairedDelimiter\ceil{\lceil}{\rceil}
\DeclarePairedDelimiter\floor{\lfloor}{\rfloor}
\newcommand{\true} {\textsf{true}}
\newcommand{\false} {\textsf{false}}
\newcommand{\Even} {\textsf{Even}}
\newcommand{\Odd} {\textsf{Odd}}
\newcommand{\subst}[2]{\{#1 \mapsto #2\}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
168
\newcommand{\subs}[2]{\{#2/#1\}}
169
\newcommand{\fv}{\textsf{fv}}
Mickael Laurent's avatar
Mickael Laurent committed
170
171
\newcommand{\bv}{\textsf{bv}}
\newcommand{\var}{\textsf{var}}
172

Giuseppe Castagna's avatar
Giuseppe Castagna committed
173
\newcommand{\Refinef}{\textsf{\textup{Refine}}}
174
\newcommand{\Refine}[2]{\ensuremath{\Refinef_{#1}(#2)}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
175
\newcommand{\RefineStep}[1]{\textsf{\textup{RefineStep}}_{#1}}
176

Giuseppe Castagna's avatar
Giuseppe Castagna committed
177

Giuseppe Castagna's avatar
Giuseppe Castagna committed
178
\newcommand{\constrf}{\textsf{\textup{Constr}}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
179
\newcommand{\constr}[2]{\constrf_{#2}(#1)}
180
%\newcommand{\env}[1]{\textsf{Env}_{#1}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
181
\newcommand{\env}[1]{\textsf{\textup{Intertype}}_{#1}}
182
183
184

\newcommand{\cons}[2]{{#1}\textsf{::}{#2}}
\newcommand{\fixpoint}{\textsf{gfp}}
185
\newcommand{\reduces}{\leadsto}
186
\newcommand{\xleadsto}[1]{\overset{#1}{\leadsto}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
187
\newcommand{\idleadsto}[0]{\xleadsto{\textit{Id}}}
188
\newcommand{\uleadsto}[0]{\xleadsto{\large{\textbf{\_}}}}
189
190
191
\newcommand{\values}[0]{\mathcal{V}}
\newcommand{\valsemantic}[1]{{\llbracket #1 \rrbracket}_{\values}}
\newcommand{\vvdash}[0]{\vdash_\values}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
192
193
194
\newcommand{\AR}{-Alg}%\ensuremath{_\mathcal{A}}}
\newcommand{\eras}[1]{\lceil#1\rceil}
\newcommand{\norm}[1]{\textsf{N}(#1)}
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
%\newcommand{\norm}[1]{\textsf{Norm}(#1)}
\newcommand{\semantic}[1]{{\llbracket #1 \rrbracket}}
\newcommand{\tenv}[0]{\vec \alpha}

\newcommand{\make@circled}[2]{%
  \ooalign{$\m@th#1\smallbigcirc{#1}$\cr\hidewidth$\m@th#1#2$\hidewidth\cr}%
}
\newcommand{\smallbigcirc}[1]{%
  \vcenter{\hbox{\scalebox{0.77778}{$\m@th#1\bigcirc$}}}%
}

\newcommand{\tsand}{\mathbin{\mathpalette\make@circled\wedge}}
\newcommand{\tsor}{\mathbin{\mathpalette\make@circled\vee}}
%\newcommand{\tstimes}{\otimes}
\newcommand{\tstimes}{\mathbin{\mathpalette\make@circled\times}}
\newcommand{\tsempty}{\Omega}
\newcommand{\tsfun}[1]{{[}#1]}
\newcommand{\tsfunone}[2]{{[}\arrow {#1} {#2}]}
\newcommand{\ts}{\mathbbm{t}}
\newcommand{\tsint}[1]{\textbf{\textup{\{}}#1\textbf{\textup{\}}}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
215
\newcommand{\tsrep}[1]{\textsf{\textup{Repr}}(#1)}
Mickael Laurent's avatar
Mickael Laurent committed
216

Giuseppe Castagna's avatar
Giuseppe Castagna committed
217
\newcommand{\vdashA}{\vdash_{\!\scriptscriptstyle\mathcal{A}}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
218
\newcommand{\vdashAts}{\vdash_{\!\scriptscriptstyle\mathcal{A}_\text{ts}}}
219
\newcommand{\vdashp}{\vdash^{\texttt{Path}}}
220
221
\newcommand{\pvdash}[3]{\vdashp_{#1,#2,#3}}%\mathcal{P}
\newcommand{\evdash}[2]{\vdash^{\texttt{Env}}_{#1,#2}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
222
223
224
225

\DeclareMathSymbol{\qm}{\mathalpha}{operators}{"3F}
\DeclareMathAlphabet{\mathbbm}{U}{bbold}{m}{n}
\newcommand{\dyn}{\ensuremath{\mathbbm{\qm}}}
226
\newcommand{\Aa}{\ensuremath{_{\scriptscriptstyle\mathcal{A}}}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
227
\newcommand{\Aats}{\ensuremath{_{\scriptscriptstyle\mathcal{A}_\text{ts}}}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
228

229
230
\newcommand{\leqA}{\leq_{\!\scriptscriptstyle\mathcal{A}}}

Giuseppe Castagna's avatar
Giuseppe Castagna committed
231
%%%%%% Dirty hack to save some space on the first page
Giuseppe Castagna's avatar
Giuseppe Castagna committed
232

233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
%% \def\copyrightpermissionfootnoterule{}
%% \def\maketitle{%
%%   \if@ACM@anonymous
%%     % Anonymize omission of \author-s
%%     \ifnum\num@authorgroups=0\author{}\fi
%%   \fi
%%   \begingroup
%%   \let\@footnotemark\@footnotemark@nolink
%%   \let\@footnotetext\@footnotetext@nolink
%%   \def\@makefnmark{\hbox{\@textsuperscript{\@thefnmark}}}%
%%   \@mktitle\if@ACM@sigchiamode\else\@mkauthors\fi\@mkteasers
%%   \@printtopmatter
%%   \if@ACM@sigchiamode\@mkauthors\fi
%%   \setcounter{footnote}{0}%
%%   \@titlenotes
%%   \@subtitlenotes
%%   \@authornotes
%%   \let\@makefnmark\relax
%%   \let\@thefnmark\relax
%%   \let\@makefntext\noindent
%%   \ifx\@empty\thankses\else
%%     \footnotetextauthorsaddresses{%
%%       \def\par{\let\par\@par}\parindent\z@\@setthanks}%
%%   \fi
%%   \ifx\@empty\@authorsaddresses\else
%%      \if@ACM@anonymous\else
%%        \if@ACM@journal
%%          \footnotetextauthorsaddresses{%
%%            \def\par{\let\par\@par}\parindent\z@\@setauthorsaddresses}%
%%        \fi
%%      \fi
%%   \fi
%%   \endgroup
%%   \setcounter{footnote}{0}%
%%   \@mkabstract
%%   \if@ACM@printccs
%%     \ifx\@concepts\@empty\else\bgroup
%%       {\@specialsection{CCS Concepts}%
%%          \@concepts\par}\egroup
%%      \fi
%%    \fi
%%   \andify\authors
%%   \andify\shortauthors
%%   \global\let\authors=\authors
%%   \global\let\shortauthors=\shortauthors
%%   \if@ACM@printacmref
%%      \@mkbibcitation
%%   \fi
%%   \hypersetup{%
%%     pdfauthor={\authors},
%%     pdftitle={\@title},
%%     pdfsubject={\@concepts},
%%     pdfkeywords={\@keywords},
%%     pdfcreator={LaTeX with acmart
%%       \csname ver@acmart.cls\endcsname\space
%%       and hyperref
%%       \csname ver@hyperref.sty\endcsname}}%
%%   \global\@topnum\z@ % this prevents floats from falling
%%                      % at the top of page 1
%%   \global\@botnum\z@ % we do not want them to be on the bottom either
%%   \@printendtopmatter
%%   \@afterindentfalse
%%   \@afterheading
%% }
297

298
299
300
301
%% \newcommand{\bbGamma}{{\mathpalette\makebbGamma\relax}}
%% \newcommand{\makebbGamma}[2]{%
%%   \raisebox{\depth}{\scalebox{1}[-1]{$\mathsurround=0pt#1\mathbb{L}$}}%
%% }
302

303
304
305
306
307
308
309
310
311
312
313
314
%% \newcommand{\Raux}[1]{\textsf{Aux}_{#1}}
%% \newcommand{\RRefine}[1]{\textsf{Refine}_{#1}}
%% \newcommand{\lfp}[1]{\textsf{lfp}_{#1}}
%% \newcommand{\RRefineStep}[1]{\textsf{RefineStep}_{#1}}
%% \newcommand{\dt}[0]{\mathbb{T}}
%% \newcommand{\fvdash}[2]{\vdash^{\texttt{Env}\rightarrow}_{#1,#2}}
%% \newcommand{\bvdash}[2]{\vdash^{\texttt{Env}\leftarrow}_{#1,#2}}
%% % \newcommand{\ufvdash}[3]{{\underset{#1}\vdash}^{\texttt{Env}\rightarrow}_{#2,#3}}
%% % \newcommand{\ubvdash}[3]{{\underset{#1}\vdash}^{\texttt{Env}\leftarrow}_{#2,#3}}
%% \newcommand{\ufvdash}[3]{\vdash^{{#1},\texttt{ Env}\rightarrow}_{#2,#3}}
%% \newcommand{\ubvdash}[3]{\vdash^{{#1},\texttt{ Env}\leftarrow}_{#2,#3}}
%% \newcommand{\cvdash}[0]{\vdash^{\texttt{Choices}}}
Mickael Laurent's avatar
Mickael Laurent committed
315

316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
%% \newcommand{\ct}[0]{\mathcal{C}}
%% \newcommand{\Gammap}[0]{{\Gamma'}}
%% \newcommand{\avdash}[2]{\vdash_{#1,\ #2}}
%% \newcommand{\bt}[0]{\texttt{Backtrack}}
%% \newcommand{\Gammas}[0]{\bbGamma}
%% \newcommand{\Tree}[0]{\texttt{T}}
%% \newcommand{\Node}[0]{\texttt{N}}
%% \newcommand{\Leaf}[0]{\texttt{L}}
%% \newcommand{\tree}[0]{\mathcal{T}}
%% \newcommand{\ttype}[0]{\texttt{type}}
%% \newcommand{\tleaves}[0]{\texttt{leaves}}
%% \newcommand{\tnodes}[0]{\texttt{nodes}}
%% \newcommand{\tlabels}[0]{\texttt{labels}}
%% \newcommand{\tflatten}[0]{\texttt{flatten}}
%% \newcommand{\btr}[0]{\blacktriangleright}
331

332
333
334
%% \makeatletter % allow us to mention @-commands
%% \def\arcr{\@arraycr}
%% \makeatother