\usepackage[english]{babel}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc} 
\usepackage{upgreek}
\usepackage{paralist}
\usepackage{enumitem}
\usepackage{caption}
\usepackage{mdframed}
\usepackage{subcaption}
\usepackage{textcomp}
\usepackage{bbding}
% \usepackage{subfig} 
\usepackage[numbers,longnamesfirst]{natbib}
% ------------------------------------------------------------------------
\usepackage{xspace}
\usepackage{xcolor}
\usepackage[ruled,vlined]{algorithm2e}
\usepackage{nicefrac}
\usepackage{bbm}
\usepackage{graphicx}
% ------------------------------------------------------------------------

% ------------------------------------------------------------------------
\usepackage{mathpartir}
\usepackage{bbold}
\usepackage{yfonts}
\usepackage{amsmath,amsfonts,amssymb}

% ------------------------------------------------------------------------
\usepackage{todonotes}
\newcommand{\gb}[1]{\ifdraft\todo[author=Gilles,color=green, inline]{#1}\fi}
\newcommand{\te}[1]{\ifdraft\todo[author=Thomas,color=yellow, inline]{#1}\fi}
\newcommand{\jh}[1]{\ifdraft\todo[author=Justin, inline]{#1}\fi}
\newcommand{\lf}[1]{\ifdraft\todo[author=Luis, color=cyan, inline]{#1}\fi}

% ------------------------------------------------------------------------
\usepackage{xargs}
% \newcommandx{\note}[2][1=]{\todo[inline,linecolor=red,backgroundcolor=red!25,bordercolor=red,#1]{#2}}

% ------------------------------------------------------------------------
\newtheorem{thm}{Theorem}
\newtheorem{defi}{Definition}
\newtheorem{lem}[thm]{Lemma}
\newtheorem{prop}[thm]{Proposition}
\newtheorem{cor}[thm]{Corollary}
\newtheorem{conj}[thm]{Conjecture}

\newcommand{\rname}[1]{[{\sc #1}]}
% ------------------------------------------------------------------------
\DeclareMathOperator{\id}{id}

\newcommand{\Dist}{\ensuremath{\mathbf{Distr}}}
\newcommand{\dom}{\text{dom}}
\newcommand{\dc}[1]{\langle{#1} \rangle}
\newcommand{\dg}[2]{{#1}_{{[}{#2}{]}}}
\newcommand{\ar}[2]{\nicefrac{#1}{#2}}
\newcommand{\pr}[1]{\oint{#1}}
\newcommand{\ex}[1]{\mathbb{E}[#1]}
\newcommand{\fint}[2]{\int_{#1}\!{#2}}
\newcommand{\aform}{\ensuremath{\phi}}
\newcommand{\bform}{\ensuremath{\psi}}
\newcommand{\genp}{\ensuremath{\mathcal{P}}}
\newcommand{\genq}{\ensuremath{\mathcal{Q}}}
\newcommand{\True}{\ensuremath{\mathop{\top}}}
\newcommand{\False}{\ensuremath{\mathop{\perp}}}
\newcommand{\Set}[1]{\{#1\}}

% Sets
\newcommand{\Nats}{\mathbb{N}}
\newcommand{\Ints}{\mathbb{Z}}
\newcommand{\Reals}{\mathbb{R}}

% Distributions
\newcommand{\bernD}{\mathbf{Bern}}
\newcommand{\geomD}{\mathbf{Geom}}
\newcommand{\unifD}{\mathbf{Unif}}
\newcommand{\normD}{\mathbf{Norm}}


\newcommand{\bd}[1]{\mathbf{#1}}
\newcommand{\NN}{\mathbf{N}}
\newcommand{\ZZ}{\mathbf{Z}}
\newcommand{\RR}{\mathbf{R}}
\newcommand{\BB}{\mathbf{B}}
\newcommand{\FF}{\mathbf{F}}
\newcommand{\T}{\mathbf{T}}
\newcommand{\Mes}{\mathbf{Mes}}
\newcommand{\Mem}{\mathsf{Mem}}


\newcommand{\rv}[1]{\mathfrak{#1}}
\newcommand{\A}{\mathfrak{A}}
\newcommand{\B}{\mathfrak{B}}
\newcommand{\M}{\mathfrak{M}}
\newcommand{\X}{\mathfrak{X}}
\newcommand{\Y}{\mathfrak{Y}}
\newcommand{\Z}{\mathfrak{Z}}

\newcommand{\dif} {\mathrm{d}}
\newcommand{\Prob}{\mathbb{P}}

\newcommand{\ExpSymb}{\mathbf{E}}
\newcommand{\Exp}[1]{\ExpSymb[#1]}
\newcommand{\CondExp}[2]{\ExpSymb[#1 \mid #2]}
\newcommand{\indFn}[1]{\mathbb{1}_{\{#1\}}}
\newcommand{\SigmaAlgebra}[1][F]{\mathcal{#1}}

\newcommand{\col}[1]{\left[\begin{matrix} #1 \end{matrix} \right]}
\newcommand{\comb}[2]{\binom{#1^2 + #2^2}{#1+#2}}

\newcommand\q{[\![}
\newcommand\p{]\!]}
\newcommand\Sem[1]{\q #1 \p}
\newcommand{\dsem}[2]{\denot{#2}_{#1}}
\newcommand\bind[2]{\mathrm{bind} (#1, #2)} 
\newcommand\unit[1]{\mathrm{unit} (#1)}

\newcommand{\pWhile}{\textsf{pWhile}\xspace}
\newcommand{\expr}{\mathcal{E}}
\newcommand{\dexpr}{\mathcal{D}}

% Language

\newcommand{\abort}{\mathsf{abort}}
\newcommand{\skp}{\mathsf{skip}}
\newcommand{\Var}{\mathcal{X}}
\newcommand{\SVar}{\mathcal{S}}
\newcommand{\Expr}{\mathcal{E}}
\newcommand{\DExpr}{\mathcal{DE}}
\newcommand{\Instr}{\mathcal{I}}
\newcommand{\Cmd}{\mathcal{C}}
\newcommand{\Seq}[2]{#1;\ #2}
\newcommand{\while}[2]{\mathsf{while}\ #1\ \mathsf{do}\ #2}
\newcommand{\ifstmt}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3}
\newcommand{\Condt}[2]{\mathsf{if}\ #1\ \mathsf{then}\ #2}
\newcommand{\Skip}{\mathsf{skip}}
\newcommand{\Ass}[2]{#1 \leftarrow #2}
\newcommand{\Rand}[2]{#1 \stackrel{\raisebox{-.25ex}[.25ex]%
 {\tiny $\mathdollar$}}{\raisebox{-.2ex}[.2ex]{$\leftarrow$}} #2}
\newcommand{\Cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3}
\newcommand{\WWhile}[2]{\mathsf{while}\ #1\ \mathsf{do}\ #2}
\newcommand{\Call}[3]{#1 \leftarrow #2\mathsf{(}#3\mathsf{)}}
\newcommand{\rnd}[2]{#1 \stackrel{\raisebox{-.25ex}[.25ex]{\tiny $\mathdollar$}}{\raisebox{-.2ex}[.2ex]{$\leftarrow$}} #2}

\renewcommand{\Pr}[2]{\mathrm{Pr}_{#1}{\left[ #2 \right]}}

\newcommand{\pre}{\Psi}
\newcommand{\post}{\Phi}
\newcommand{\Inv}{\varphi}


\newcommand{\Equiv}[4]{%
  \vDash #1 \sim {#2}: {#3} \Rightarrow {#4} }

\newcommand{\infr}[2]{
{\renewcommand{\arraystretch}{1.1}
\begin{array}{c}
{#1}\\
\hline
{#2}
\end{array}}}

\newcommand{\side}[1]{\langle #1 \rangle}
\newcommand{\sidel}{\side{1}}
\newcommand{\sider}{\side{2}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Listings setup
\usepackage{listings}

% Nice looking setup (stolen from TeX gurus), requires the beramono
% package thou.
\usepackage[T1]{fontenc}
\usepackage{microtype}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Solution 1
% \usepackage[scaled]{beramono}
% \newcommand\Small{\fontsize{7pt}{7.2pt}\selectfont}
% \newcommand*\LSTfont{\Small\ttfamily\SetTracking{encoding=*}{-60}\lsstyle}
% End solution 1
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Solution 2 (variation on 1)
\usepackage[scaled]{beramono}
\newcommand\Small{\fontsize{8.2pt}{8.4pt}\selectfont}
\newcommand*\LSTfont{\Small\ttfamily\SetTracking{encoding=*}{-60}\lsstyle}
% End solution 2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Solution 3 (Using inconsolata)
% \usepackage{inconsolata}
% \newcommand\Small{\fontsize{8.3pt}{8.5pt}\selectfont}
% \newcommand*\LSTfont{\Small\ttfamily\SetTracking{encoding=*}{-60}\lsstyle}
% End solution 3
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\lstrnd{\stackrel{\raisebox{-.15ex}{\ensuremath{\scriptscriptstyle\$}}}{\raisebox{-.2ex}{\ensuremath{\leftarrow}}}}

\lstset{
         language=ML,
         basicstyle=\LSTfont\small,
         % basicstyle=\ttfamily\footnotesize,
         % numbersep=5pt,
         % tabsize=2,
         extendedchars=true,
         breaklines=true,
         keywordstyle=\bfseries,
         morekeywords={param,array,set,for,to,fi,var,return},
         % keywordstyle=\color{red},
         % frame=b,
         mathescape=true,
         literate={->}{{$\to$}}1%
                  {=>}{{$\Rightarrow$}}1%
                  {-->}{{$\qquad \leadsto$}}1%
                  {~~}{{$\;\lstrnd\,$}}1%
                  {:=}{{$\;\leftarrow\,$}}1%
                  {<>}{{$\;\neq$}}2%
                  {emptyset}{{$\emptyset$}}1,
         stringstyle=\ttfamily,
         showspaces=false,
         showtabs=false,
         xleftmargin=8pt,
         showstringspaces=false
 }

\newcommand{\lstt}[1]{\mbox{\LSTfont #1}}
\newcommand\lstiny{\fontsize{6.6pt}{6.8pt}\selectfont}
\newcommand{\lstts}[1]{\mbox{\lstiny\ttfamily\SetTracking{encoding=*}{-60}\lsstyle #1}}
 
% End listings setup
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{xcolor}
\definecolor{DarkGreen}{rgb}{0.1,0.5,0.1}
\definecolor{DarkRed}{rgb}{0.5,0.1,0.1}
\definecolor{DarkBlue}{rgb}{0.1,0.1,0.5}
\usepackage{hyperref}
\hypersetup{
    unicode=false,          % non-Latin characters in Acrobat's bookmarks
    pdftoolbar=true,        % show Acrobat toolbar?
    pdfmenubar=true,        % show Acrobat menu?
    pdffitwindow=false,      % page fit to window when opened
    pdftitle={},    % title
    pdfauthor={}
    pdfsubject={},   % subject of the document
    pdfnewwindow=true,      % links in new window
    pdfkeywords={keywords}, % list of keywords
    colorlinks=true,       % false: boxed links; true: colored links
    linkcolor=DarkRed,          % color of internal links
    citecolor=DarkGreen,        % color of links to bibliography
    filecolor=DarkRed,      % color of file links
    urlcolor=DarkBlue,          % color of external links
}

\usepackage{cleveref}
\crefname{section}{\S}{\S}
\Crefname{section}{\S}{\S}

\crefname{prop}{proposition}{propositions}
\Crefname{prop}{Proposition}{Propositions}

\crefname{lem}{lemma}{lemmas}
\Crefname{lem}{Lemma}{Lemmas}

\crefname{thm}{theorem}{theorems}
\Crefname{thm}{Theorem}{Theorems}

\crefname{defi}{definition}{definitions}
\Crefname{defi}{Definition}{Definitions}