%\newcommand{\ie}{\textit{i.e.}}
\newcommand{\SET}[1]{\ensuremath{\{#1\}}}

\newcommand{\Ok}[2]{\ensuremath{#1 \vdash #2 ~\, \mathsf{ok}}}
\newcommand{\OkG}[1]{\ensuremath{\Gamma \vdash #1 ~\, \mathsf{ok}}}

\newcommand{\num}{\ensuremath{\mathtt{num}}}
\newcommand{\plus}{\ensuremath{\mathtt{plus}}}
\newcommand{\Times}{\ensuremath{\mathtt{times}}}
\newcommand{\Let}{\ensuremath{\mathtt{let}}}

\newcommand{\Trans}[2]{#1 \, \mapsto \, #2}

\newcommand{\poset}[2]{\ensuremath{\langle #1,\,#2 \rangle}}

\newcommand{\Nat}{\ensuremath{\mathbb{N}}}
\newcommand{\Zero}{\ensuremath{\mathrm{Z}}}
\newcommand{\Succ}{\ensuremath{\mathrm{S}}}

%               
% inference rules                                                           
\newcommand{\infer}[2]{\frac{\;{#1}\;}{\;{#2}\;}}

\newcommand{\inferl}[3]{\frac{\;{#2}\;}{\;{#3}\;} \quad (#1)}

\newcommand{\INFER}[3][]{%
  \begin{equation}\label{#1}
      \infer{#2}{#3}
  \end{equation}}

\newcommand{\INFERL}[3][]{%
  \begin{displaymath}
      \inferl{#1}{#2}{#3}
  \end{displaymath}}                     
