finite-dtypes.sty

{\catcode`\/=13\gdef\activeSlash{\catcode`\/=13\def/##1/{\kw{##1}}}}

\def\kw#1{%
  \expandafter\ifx\csname#1\endcsname\relax
    \mathsf{#1}%
  \else
    \csname#1\endcsname
  \fi
}

\def\IF{\mathsf{if}\,}
\def\THEN{\,\mathsf{then}\,}
\def\ELSE{\,\mathsf{else}\,}

\def\SUM{\mathsf{sum}\;}

\def\WHEN{\mathrm{when}\;}
\def\AND{\;\mathrm{and}\;}

\def\reference{\mathsf{\&}}

\def\succ{\mathsf{succ}}
\def\ss{\mathsf{ss}}

\def\indent{{\quad}}

\def\fn{\mathop\lambda}

\def\zero{\mathsf{0}}
\def\zerop{\mathsf{0}}
\def\one{\mathsf{1}}
\def\onep{\mathsf{1}}
\def\unitp{\mathsf{unit}}
\def\boolp{\mathsf{bool}}
\def\prodp{\prod}
\def\succp{\mathsf{succ}}
\def\binary{\mathsf{binary}}

\newenvironment{code}
  {\activeSlash\[\begin{array}{r@{\,}l@{\,}l}\ignorespaces}
  {\end{array}\]\ignorespacesafterend}

\newenvironment{tinyverb}
  {\fontsize{6}{6}\verbatim}
  {\endverbatim}

\def\subsection{\@startsection
  {subsection}
  {2}
  {\z@}
  {-.5\baselineskip \@plus -2\p@ \@minus -.2\p@ }
  {-.5em}
  {\subsectionfont}}

\def\subsectionfont#1{\textbf{#1.}}

\setcounter{secnumdepth}{1}