\documentclass[a4paper,11pt]{memoir}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{booktabs}
\usepackage{color}
\usepackage{enumitem}
\usepackage{fancyvrb}
\usepackage[sfdefault]{FiraSans}
\usepackage{graphicx}
\usepackage[a4paper,pdftex,pdfkeywords={},pdfborder={0 0 0},draft=false,
  bookmarksnumbered,bookmarks,bookmarksdepth=2,bookmarksopenlevel=0,
  bookmarksopen]{hyperref}
\usepackage[utf8x]{inputenc}
\usepackage{listings}
\usepackage{prftree}
\usepackage{stmaryrd}
\usepackage{tabularx}
\usepackage{wasysym}

\usepackage{tikz}
\usetikzlibrary{graphs, arrows}

\makeatletter

%% Proof trees

\prfinterspace=2em

%% Lean code

\def\lstlanguagefiles{lstleanbw.tex}

\renewcommand\lst@visiblespace{\ensuremath{\;}}
\newcommand\li{\lstinline[showspaces=true]}

\lstset{
  language=lean,
  xleftmargin=\leftmargin,
  includerangemarker=false,
  rangebeginprefix=--quo\ ,
  rangeendprefix=--ou}

%% Layout

\setlength{\textwidth}{140mm}
\setlength{\spinemargin}{35mm}
\setlength{\foremargin}{35mm}
%\setlength{\spinemargin}{37.5mm}
%\setlength{\foremargin}{32.5mm}
\setlength{\uppermargin}{32.5mm}
\setlength{\textheight}{232mm}
\checkandfixthelayout

\setitemize{noitemsep,itemsep=\smallskipamount,topsep=0.5\smallskipamount} % ,parsep=0pt,partopsep=0pt}
%\newcommand\betweenlistings{\vspace{-\smallskipamount}}  %% approximate
\let\betweenlistings=\relax

\hyphenation{meta-programming}

%% Definitions

\include{defs}

%% end of prelude

\begin{document}

\frontmatter
\pagenumbering{roman}   % i, ii, iii, iv, ...
\setcounter{page}{1}

\thispagestyle{empty}

{\begingroup
\vspace*{0.08\textheight}
\noindent
\hspace*{0.3\textwidth}{\Large\strut Tim Baanen} \\[.5\jot]
\hspace*{0.3\textwidth}{\Large\strut Alexander Bentkamp} \\[.5\jot]
\hspace*{0.3\textwidth}{\Large\strut Jasmin Blanchette} \\[.5\jot]
\hspace*{0.3\textwidth}{\Large\strut Johannes H\"olzl} \\[0.16\textheight]
\hspace*{0.3\textwidth}{\Huge\bfseries\itshape Logical Verification}\par
{\raggedleft\Huge\bfseries\itshape in Lean\hspace*{0.0225\textwidth}\par}
\bigskip
\bigskip
\noindent
\hspace*{0.3\textwidth}{\Large\bfseries\itshape 2019 Edition} \\[\jot]
\hspace*{0.3\textwidth}{(\today)}
\vfill
\noindent
\hspace*{0.3\textwidth}{\includegraphics[width=0.1\textwidth]{images/lfwd_icon_black}\par\medskip}
\noindent
\hspace*{0.3\textwidth}{\Large
\href{https://lean-forward.github.io/logical-verification/2019}{lean-forward.github.io/}\par}
{\raggedleft\Large
\href{https://lean-forward.github.io/logical-verification/2019}{logical-verification/2019}\hspace*{0.0225\textwidth}\par}
\vspace*{0.08\textheight}
\endgroup}

\newpage

~

\newpage

\pagestyle{plain}
\setcounter{tocdepth}{1}

\tableofcontents

\include{preface}

\thispagestyle{plain}
\pagestyle{loveheadings}

\mainmatter
\pagenumbering{arabic}  % 1, 2, 3, 4, ...
\setcounter{page}{1}

\part{Basics}

\include{ch01-definitions-and-lemma-statements}
\include{ch02-tactical-proofs}
\include{ch03-structured-proofs-and-proof-terms}

\part{Functional--Logic Programming}

\include{ch04-functional-programming}
\include{ch05-inductive-predicates}
\include{ch06-monads}
\include{ch07-metaprogramming}

\part{Program Semantics}

\include{ch08-operational-semantics}
\include{ch09-hoare-logic}
\include{ch10-denotational-semantics}

\part{Mathematics}

\include{ch11-logical-foundations-of-mathematics}
\include{ch12-basic-mathematical-structures}
\include{ch13-rational-and-real-numbers}

\raggedright

\bibliography{bib}{}
\bibliographystyle{abbrv}

\end{document}
