\usepackage{times}
%-------------------------
% the following magic makes the tt font in math mode be the same as the
% normal tt font (i.e., Courier)
%
\SetMathAlphabet{\mathtt}{normal}{OT1}{pcr}{n}{n}
\SetMathAlphabet{\mathtt}{bold}{OT1}{pcr}{bx}{n}
%-------------------------

\usepackage{amsmath}

\newcommand{\NOTE}[1]{%
  \par\leavevmode\noindent\textbf{[[ #1 ]]}\par\leavevmode\noindent}
\newcommand{\CUT}[1]{}
\newcommand{\SIDENOTE}[1]{%
  \marginpar{\tiny\raggedright{#1}}}

\newcommand{\appref}[1]{Appendix~\ref{#1}}
\newcommand{\chapref}[1]{Chapter~\ref{#1}}
\newcommand{\secref}[1]{Section~\ref{#1}}
\newcommand{\tblref}[1]{Table~\ref{#1}}
\newcommand{\figref}[1]{Figure~\ref{#1}}
\newcommand{\listingref}[1]{Listing~\ref{#1}}
\newcommand{\pref}[1]{{page~\pageref{#1}}}
\newcommand{\defref}[1]{Definition~\ref{#1}}
\newcommand{\ruleref}[1]{Rule~\ref{#1}}

\newcommand{\eg}{{\em e.g.}}
\newcommand{\cf}{{\em cf.}}
\newcommand{\ie}{{\em i.e.}}
\newcommand{\etc}{{\em etc.\/}}
\newcommand{\naive}{na\"{\i}ve}
\newcommand{\ala}{{\em \`{a} la\/}}
\newcommand{\etal}{{\em et al.\/}}
\newcommand{\role}{r\^{o}le}
\newcommand{\vs}{{\em vs.}}
\newcommand{\forte}{{fort\'{e}\/}}

%
% font commands
\providecommand{\bftt}[1]{{\ttfamily\bfseries{}#1}}
\providecommand{\ittt}[1]{{\ttfamily\itshape{}#1}}
\providecommand{\kw}[1]{\bftt{#1}}
\providecommand{\nt}[1]{{\rmfamily\itshape{#1}}}
\providecommand{\term}[1]{{\sffamily{#1}}}
\providecommand{\tyvar}[1]{\ittt{#1}}
%
% math-mode versions
\providecommand{\mkw}[1]{\ensuremath{\text{\kw{#1}}}}
\providecommand{\mnt}[1]{\ensuremath{\text{\nt{#1}}}}
\providecommand{\mterm}[1]{\ensuremath{\text{\term{#1}}}}
\providecommand{\mtyvar}[1]{\ensuremath{\text{\tyvar{#1}}}}

% braces (in math mode)
\newcommand{\LCB}{\mkw{\{}}
\newcommand{\RCB}{\mkw{\}}}

% underscore
\newcommand{\US}{\char`\_}

%%%%%
% Some common math notation
%

% double brackets
\newcommand{\LDB}{\ensuremath{[\mskip -3mu [}}
\newcommand{\RDB}{\ensuremath{]\mskip -3mu ]}}

\newcommand{\dom}{\ensuremath{\mathrm{dom}}}
\newcommand{\rng}{\ensuremath{\mathrm{rng}}}

% sets
\newcommand{\SET}[1]{\ensuremath{\{#1\}}}
\newcommand{\Fin}{\textrm{Fin}}     % finite power set
\newcommand{\DISJOINT}[2]{\ensuremath{#1 \pitchfork #2}}
\newcommand{\finsubset}{\mathrel{\stackrel{\textrm{fin}}{\subset}}}

% finite maps
\newcommand{\finmap}{\mathrel{\stackrel{\textrm{fin}}{\rightarrow}}}
\newcommand{\MAP}[2]{\SET{#1 \mapsto #2}}
\newcommand{\EXTEND}[2]{\ensuremath{#1{\pm}#2}}
\newcommand{\EXTENDone}[3]{\EXTEND{#1}{\MAP{#2}{#3}}}
\newcommand{\SUBST}[3]{\ensuremath{#1[#2\mapsto{}#3]}}
\newcommand{\SUBSTTWO}[5]{\ensuremath{#1[#2\mapsto{}#3,#4\mapsto{}#5]}}

% inference rules
\newcommand{\infer}[2]{\frac{\;{#2}\;}{\;{#1}\;}}
%
% labeled inference rule:
%   \INFER{name}{label}{conclusion}{assumption}
%
\newcommand{\INFER}[2]{%                                                      
  \begin{equation*}
    \infer{#1}{#2}                                                            
  \end{equation*}}                                                               

% natural numbers
%
\newcommand{\Nat}{\mathcal{N}}

% Diderot types
%
\newcommand{\TYbool}{\mathbf{bool}}
\newcommand{\TYint}{\mathbf{int}}
\newcommand{\TYreal}{\mathbf{real}}
\newcommand{\TYrawten}[3]{\mathbf{rawten}\langle{}#1,#2,#3\rangle{}}
\newcommand{\TYtensor}[2]{\mathbf{tensor}\langle{}#1,#2\rangle{}}
\newcommand{\TYmatrix}[2]{\mathbf{matrix}\langle{}#1,#2\rangle{}}
\newcommand{\TYimage}[2]{\mathbf{image}_{#1}\langle{}#2\rangle{}}
\newcommand{\TYkern}[1]{\mathbf{kern}^{#1}}
\newcommand{\TYfield}[3]{\mathbf{field}^{#1}_{#2}\langle{}#3\rangle{}}
\newcommand{\TYvec}[1]{\mathbf{vec}_{#1}}

% Diderot operators
%
\newcommand{\OPdiff}{\mathbf{D}}
\newcommand{\OPconvolve}{\mathbf{convolve}}

% typing judgments
%
\newcommand{\HasTy}[2]{#1 : #2}
\newcommand{\UnopTy}[3]{\HasTy{#1}{#2 \rightarrow #3}}
\newcommand{\BinopTy}[4]{\HasTy{#1}{#2 \times #3 \rightarrow #4}}