\newcommand{\cf}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\stepsto}{\ensuremath{\rightarrow}}
\newcommand{\evals}[2]{\cf{{#1} \Downarrow {#2}}}

% Miscellaneous latex commands for TAPL stuff in slides

\newcommand{\pA}{\mathrel{\vdash\!\!\!\!\raisebox{.28ex}{$\scriptscriptstyle \blacktriangleright$}}}
\newcommand{\GpA}{\Gamma\pA}
\newcommand{\FAIL}{{\mathit fail}}
\newcommand{\subtype}{\kw{subtype}}
\newcommand{\highlight}{}

\newcommand{\smallaxiom}[1]{
  \ensuremath{\displaystyle
      {#1}
  }
}
\newcommand{\smallrule}[2]{
  \ensuremath{\displaystyle
    \frac
      {#1}
      {#2}
  }
}

\newcommand{\inductionprinciple}[4]
  {\vspace{-1ex}\begin{quote}
    {
    \begin{tabbing}
    If, for each #2, \\
    \qquad \= we can show \quad \= \kill
           \> given $P(#3)$ #4 \\
           \> we can show  $P(#1)$, \\
    then $P(#1)$ holds for all $#1$.  
    \end{tabbing}
    }
    \end{quote}}
\newcommand{\newinductionprinciple}[5]
  {\vspace{-1ex}\begin{quote}
    {
    \begin{tabbing}
    If, for each #2{} #3, \\
    \qquad \= we can show \quad \= \kill
           \> given $P(#4)$ #5 \\
           \> we can show  $P(#3)$, \\
    then $P(#1)$ holds for all $#1$.  
    \end{tabbing}
    }
    \end{quote}}

\renewcommand{\P}{\ensuremath{\mathit{P}}}
\newcommand{\NAT}{\ensuremath{\mathcal{N}}}
\newcommand{\TERMS}{\ensuremath{\cal T}}
\newcommand{\BOOL}{\ensuremath{\cal B}}
\newcommand{\DERD}{\ensuremath{\cal D}}
\newcommand{\TERMSS}{\ensuremath{\cal S}}
\newcommand{\CONSTS}{\ensuremath{\mathit{Consts}}}
\newcommand{\size}{\mathit{size}}
\newcommand{\BADCONSTS}{\mathit{BadConsts}}

\newcommand{\EVAL}{\ensuremath{\mathit{Eval}}}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Some helper functions...

% A convenient way of defining relation symbols.  Each invocation of
%    \newrelation{\relname}{...body...}
% defines two commands:
%    \relname  --  a version with ``tight'' (\mathord) spacing
%    \RELNAME  --  a version with ``generous'' (\mathrel) spacing
\def\newrelation#1#2{
   % a hack from p. 331 of the TeXbook:
     \def\doit##1\endname{\uppercase{\def\@TEMPSYMNAME{##1}}}
     \expandafter\doit#1\endname
   % \typeout{Defining #1 and \@TEMPSYMNAME}
   % \@ifdefinable\name{}
   % \@ifdefinable\NAME{}
   \expandafter\newcommand\csname #1\endcsname{\mathord{#2}}
   \expandafter\newcommand\csname\@TEMPSYMNAME\endcsname{\mathrel{#2}}
   }

% A similar hack for mathematical prefix symbols
\def\newprefix#1#2{
   % a hack from p. 331 of the TeXbook:
     \def\doit##1\endname{\uppercase{\def\@TEMPSYMNAME{##1}}}
     \expandafter\doit#1\endname
   % \typeout{Defining #1 and \@TEMPSYMNAME}
   % \@ifdefinable\name{}
   % \@ifdefinable\NAME{}
   \expandafter\newcommand\csname #1\endcsname{\mathord{#2}}
   \expandafter\newcommand\csname\@TEMPSYMNAME\endcsname{\mathord{#2}\;}
   }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Names of some popular type systems

\newcommand{\FSUBlikename}[1]{{\it #1}}
\newcommand{\FOMEGASUB}{\FSUBlikename{F}$_{\leq}^{\,\omega}$}
\newcommand{\FOMEGA}{\FSUBlikename{F}$^{\,\omega}$}
\newcommand{\FSUB}{\FSUBlikename{F}$_\leq$}
\newcommand{\F}{\FSUBlikename{F}}
\newcommand{\FMEET}{\FSUBlikename{F}$_{\!\meet}$}
\newcommand{\FSUBMU}{\FSUBlikename{F}$_{\Leq\mu}$}
\newcommand{\STLCSUB}{\ensuremath{\lambda_{\mbox{\tiny \tt <:}}}}
\newcommand{\STLC}{\ensuremath{\lambda_\rightarrow}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Useful symbols

\newcommand{\eqdef}{\stackrel{{\rm def}}{=}}
\newcommand{\defeq}{\eqdef}
\newcommand{\emptycontext}{\emptyset} 
\newcommand{\lengthof}[1]{|#1|}
\newcommand{\smallminus}{-}
\newcommand{\In}{\texttt{:}}
\newcommand{\IN}{\mathrel{\mbox{\large \texttt{:}}}}
\newcommand{\Leq}{\protect\itbox{<\kern-0.13em:}}
\newcommand{\LEQ}{\mathrel{\mbox{\large \texttt{<$\!$:}}}}
\newcommand{\FV}{\kw{FV}}
\newcommand{\BV}{\kw{BV}}
\newcommand{\dom}{\kw{dom}}
\newcommand{\range}{\kw{range}}

\newcommand{\LAMBDA}{\ensuremath{\lambda}}
\def\Defn{\ensuremath{\leftrightarrow}}
\def\FORALL{\ensuremath{\forall}}
\def\EXISTS{\ensuremath{\exists}}
\def\STRUCT{\ensuremath{\cal S}\,}
\def\KNOWNAS{\ensuremath{\triangleright}\,}
\def\PI{\ensuremath{\Pi}}

\newcommand{\p}{\vdash}
\newcommand{\notp}{\not\p}
\newcommand{\Gp}{\Gamma\p}
\newprefix{Comma}{,}

\newcommand{\List}{\kw{List}}
\newcommand{\Top}{\kw{Top}}

\newcommand{\substop}[1]{[#1]} 
\newcommand{\multisubst}[1]{\substop{#1}}
\newcommand{\subst}[2]{\multisubst{#1\mapsto#2}}
\newcommand{\match}[2]{\kw{match}(#1,\,#2)}
\newcommand{\substplus}{+}
\newcommand{\emptysubst}{\multisubst{\,}}

\newrelation{Arrow}{\rightarrow}
\newrelation{TArrow}{\Rightarrow}
\newrelation{LeftArrow}{\leftarrow}
\newrelation{Times}{\,\times\,}
\newrelation{Conv}{\longleftrightarrow^\ast}
\newrelation{Eqv}{\equiv}
\newrelation{Evalone}{\longrightarrow}
\newrelation{Evalmany}{\Evalone^{\!\mbox{\raisebox{1pt}{\tiny $\ast$}}}}
\newrelation{Implies}{\Rightarrow}
\newrelation{Notin}{\notin}
\newrelation{Eq}{=}
\newrelation{Notleq}{\not{\!\!\itbox{<$\!$:}}}
\newrelation{Meet}{\wedge}
\renewcommand{\Join}{\mathord{\vee}}
\newcommand{\JOIN}{\mathrel{\vee}}

\def\tallslug{\rule[.2mm]{.17mm}{1.7mm}}
\def\smallslug{\rule[.6mm]{.17mm}{.8mm}}
\def\LCurlyBar{\ensuremath{\itbox{\char'173}\!\tallslug\,}}
\def\BarRCurly{\,\tallslug\!\itbox{\char'175}}
\def\LSquareBar{\ensuremath{\itbox{[}\hspace{-.5mm}\tallslug\hspace{.4mm}}}
\def\BarRSquare{\ensuremath{\hspace{.4mm}\tallslug\hspace{-.4mm}\itbox{]}}}
\def\LAngleBar{\ensuremath{\itbox{<}\hspace{-.4mm}\smallslug\hspace{.2mm}}}
\def\BarRAngle{\ensuremath{\hspace{.2mm}\smallslug\hspace{-.4mm}\itbox{>}}}

\newcommand{\STORE}{\ensuremath{\mu}}
\newcommand{\STORETYPING}{\ensuremath{\Sigma}}
\newcommand{\STATEMENT}{\ensuremath{{\cal J}}}
\newcommand{\DER}{\ensuremath{{\cal D}}}
\newcommand{\DERC}{\ensuremath{{\cal C}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Miscellaneous

\newcommand{\TAPL}{{\em Types and Programming Languages}}
\newcommand{\CSHARP}{\mbox{C$^\sharp$}}

\newcommand{\SECTIONREF}[1]{\S\ref{#1}}

\newcommand{\showsystems}[1]{\@unmarkedfootnotetext{#1}}

\newcommand{\kw}[1]{\mbox{\it #1}}
\newcommand{\rnsmall}[1]{\mbox{{\small \rn{#1}}}}
\newcommand{\rntiny}[1]{\mbox{{\tiny \rn{#1}}}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Indexing commands

\newcommand{\indexandsay}[1]{\index{#1}#1}
\newcommand{\indeximpl}[2][\relax]{\index{#2@{\tt #2}
    implementation#1}\index{implementations!#2@{\tt #2}#1}}
\newcommand{\indexlang}[1]{\index{#1}\index{programming languages!#1}}
\newcommand{\indexlangquiet}[1]{\indexquiet{#1}\indexquiet{programming languages!#1}}
\newcommand{\indexlangandsay}[1]{\indexlang{#1}#1}
\newcommand{\indexlangquietandsay}[1]{\indexquiet{#1}\indexquiet{programming languages!#1}#1}
\newcommand{\indexlangopen}[1]{\index{#1|(}\index{programming languages!#1|(}}
\newcommand{\indexlangclose}[1]{\index{#1|)}\index{programming languages!#1|)}}
\newcommand{\defterm}[1]{{\it #1\/}}
\newcommand{\indexterm}[2][\empty]{%
  \ifx#1\empty
    \index{#2}%
  \else
    \index{#1}%
  \fi 
  \defterm{#2}%
}
\newcommand{\indexsym}[2]{\index{ #2@$#1$\quad #2}}
\newcommand{\indextt}[2][\empty]{%
  \ifx#1\empty
    \index{#2@{\tt #2}}%
  \else
    \index{#2@{\tt #2} #1}%
  \fi
}
\newcommand{\indexit}[2][\empty]{%
  \ifx#1\empty
    \index{#2@{\it #2}}%
  \else
    \index{#2@{\it #2} #1}%
  \fi
}
\newcommand{\NAME}[2]{#1 #2}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Figures and displays

\newcommand{\bcpcaption}[2]{\ttlabel{#1}
    {\bf Figure \@currentlabel:} #2
}
\newcommand{\prefacecaption}[2]{
    \refstepcounter{ttfigure}
    {\bf Figure P-\arabic{ttfigure}:}  #2
    \label{fig:#1}%
}

\newenvironment{indentleft}
               {\list{}{}%
                \item\relax}
               {\endlist}

\newenvironment{wide}
               {\list{}{\advance\leftmargin -113pt
                        \advance\textwidth 100pt
                        \itemindent 0pt
                        \labelsep 0pt
                        \labelwidth 0pt}%
                \item\relax}
               {\endlist}

\newenvironment{widefigure}
    {\begin{figure}\begin{wide}}
    {\end{wide}\end{figure}}

\@ifundefined{begintrivarray}{
  \newenvironment{trivarray}{\begin{array}[t]{@{}llll}}{\end{array}}
}{
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Bibliography and citation formatting

\usepackage[round]{natbib}
\bibliographystyle{plainnat}
\renewcommand{\cite}{\citep*}
\newcommand{\citeterse}{\citep}
\newcommand{\citeyr}[1]{(\citeyear{#1})}
\newcommand{\citeyropen}[1]{\citeyear{#1}}
\newcommand{\longcite}[1]{\citeauthor{#1} \citeyearpar{#1}}
\newcommand{\fulllongcite}[1]{\citeauthor*{#1} \citeyearpar{#1}}
\newcommand{\citeopen}[1]{\citealp*{#1}}
\newcommand{\citeopenterse}[1]{\citealp{#1}}
\renewcommand\bibname{References}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Compact notations for TAPL-style ``XXX..YYY'' superscripts

\newcommand{\VARUPTO}[2]%
  {\ensuremath{\,^{\scriptscriptstyle \,#1\mathord{\in}\SMALLFROMTO{\mathit{1}}{#2}}}}
\newcommand{\IUPTO}[1]{\VARUPTO{i}{#1}}
\newcommand{\ONEUPTON}{\FROMTO{\mathit{1}}{n}}
\newcommand{\IUPTON}{\VARUPTO{i}{n}}
\newcommand{\AUPTOO}{\VARUPTO{a}{o}}
\newcommand{\AUPTOM}{\VARUPTO{a}{m}}
\newcommand{\IUPTOK}{\IUPTO{k}}
\newcommand{\IUPTOM}{\IUPTO{m}}
\newcommand{\JUPTOM}{\VARUPTO{j}{m}}
\newcommand{\KUPTOM}{\VARUPTO{k}{m}}
\newcommand{\JUPTOP}{\VARUPTO{j}{p}}
\newcommand{\JUPTON}{\VARUPTO{j}{n}}
\newcommand{\LUPTOQ}{\VARUPTO{l}{q}}
\newcommand{\JUPTOIMINUSONE}{\VARUPTO{j}{i\smallminus\mathit{1}}}
\newcommand{\IUPTONPLUSK}{\IUPTO{n\mathord{+}k}}
\newcommand{\IUPTOJMINUSONE}{\IUPTO{j\!\smallminus\!\mathit{1}}}
\newcommand{\KFROMJPLUSONEUPTON}%
  {\ensuremath{^{\scriptscriptstyle 
     \,k\mathord{\in}j\!\mathord{+}\!\FROMTO{\mathit{1}}{n}}}}
\newcommand{\KFROMIPLUSONEUPTON}%
  {\ensuremath{^{\scriptscriptstyle 
     \,k\mathord{\in}i\!\mathord{+}\!\FROMTO{\mathit{1}}{n}}}}

\newcommand{\DOTDOT}{\mathord{.\hspace*{-.05em}.}}
\newcommand{\SMALLDOTDOT}{\mathord{..}}
\newcommand{\FOREACH}[1]{\mbox{for each $#1$}\ \ \ \ }
\newcommand{\FOREACHIUPTON}{\FOREACH{i}}
\newcommand{\FROMTO}[2]{#1\DOTDOT#2}
\newcommand{\SMALLFROMTO}[2]{#1\SMALLDOTDOT#2}
\newcommand{\DOTDOTDOT}{...}
\newrelation{CaseArrow}{\Rightarrow}
\newcommand{\EVALONEWITH}[1]{\mathrel{\stackrel{#1}{\longrightarrow}}}
\newcommand{\GSp}{\Gamma\WITH\STORETYPING\p}
\newcommand{\WITH}{\mathrel{|}}

\newcommand{\fieldsof}[1]{\kw{fields}(#1)}
\newcommand{\methodsof}[1]{\kw{methods}(#1)}
\newcommand{\methodtypeof}[1]{\kw{mtype}(#1)}  % was methodtype
\newcommand{\methodbodyof}[1]{\kw{mbody}(#1)}  % was methodbody
\newcommand{\methodtypemaxof}[1]{\kw{mtypemax}(#1)}  % was methodtypemax
\newcommand{\CT}{\kw{CT}}
\newcommand{\STUPID}{\mbox{\it stupid warning}}
\newcommand{\UNCHECKED}{\mbox{\it unchecked warning}}
\newcommand{\cupoverride}{\oplus}
\newcommand{\nameof}[1]{\kw{name}(#1)}
\newcommand{\argtypeof}[1]{\kw{argtypes}(#1)}
\newcommand{\override}[1]{\kw{override}(#1)}
\newcommand{\validdowncast}[1]{\kw{downcast}(#1)}
\newcommand{\emptysequence}{\emptyset}