%% Packages

\PassOptionsToPackage{hyphens}{url}

\ifdefined\TABLET
  \documentclass[a5paper,12pt]{memoir}
\else
  \documentclass[a4paper,11pt]{memoir}
\fi
\usepackage[T1]{fontenc}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{booktabs}
\usepackage{color}
\usepackage{combelow}
%\usepackage{DejaVuSansMono}
\usepackage{enumitem}
\usepackage{fancyvrb}
\usepackage[sfdefault]{FiraSans}
\usepackage{graphicx}
\usepackage[pdftex,pdfkeywords={},pdfborder={0 0 0},draft=false,
  bookmarksnumbered,bookmarks,bookmarksdepth=2,bookmarksopenlevel=0,
  pdfauthor={Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes H\"olzl, and Jannis Limperg},
  pdftitle={The Hitchhiker's Guide to Logical Verification},
  bookmarksopen]{hyperref}
\usepackage{hyphenat}
\usepackage[utf8x]{inputenc}
\usepackage[procnames]{listings}
\usepackage{mathtools}
\usepackage{microtype}
\usepackage{multicol}
\usepackage{prftree}
\usepackage{ragged2e}
\usepackage[eulergreek]{sansmath}
\usepackage{stmaryrd}
\usepackage{tabularx}
\usepackage{xltabular}
\usepackage[normalem]{ulem}
\usepackage{wasysym}

\usepackage[scale=0.87]{noto}
\usepackage[medium,scale=0.8795]{FiraMono}

\usepackage{tikz}
\usetikzlibrary{graphs,arrows,shapes.geometric}

\DisableLigatures{encoding = *, family = tt*}

\makeatletter

%% Memoir sections

\setsecnumdepth{subsection}

%% Unicode

\DeclareUnicodeCharacter{10761}{\bullet}

%% Math font

\sansmath

%% URLs

\g@addto@macro{\UrlBreaks}{\UrlOrds\do\=\do\_}

%% Proof trees

\prfinterspace=2em

%% QED

\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
\penalty50\hskip1em\null\nobreak\hfil\squareforqed
\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}

%% Layout

\ifdefined\TABLET
  \newcommand\joinlistings{\vskip-0.69\baselineskip} %%% TYPESETTING
  \setlrmarginsandblock{10mm}{10mm}{*}
  \setulmarginsandblock{20mm}{15mm}{*}
  \RaggedRight
  \raggedbottom
\else
  \newcommand\joinlistings{\vskip-\baselineskip}
  \setlength{\textwidth}{140mm}
  \setlength{\spinemargin}{35mm}
  \setlength{\foremargin}{35mm}
  %\setlength{\spinemargin}{37.5mm}
  %\setlength{\foremargin}{32.5mm}
  \setlength{\uppermargin}{32.5mm}
  \setlength{\textheight}{232mm}
\fi
\checkandfixthelayout

\setitemize{noitemsep,itemsep=\smallskipamount,topsep=1.25\smallskipamount} % ,parsep=0pt,partopsep=0pt}

\let\betweenlistings=\relax

\hyphenation{meta-pro-gram meta-pro-grams meta-pro-gram-mer meta-pro-gram-mers
  meta-pro-gram-ming Web-Assem-bly Isa-belle pro-ject pro-jects Bool-ean
  Bool-eans meta-variable meta-variables Cau-chy lem-ma lem-mas lem-mata
  name-space name-spaces}

%% Header style

\makepagestyle{loveheadings}
\makeevenhead{loveheadings}{\normalfont{\thepage}}{}{\normalfont\slshape\leftmark}
\makeoddhead{loveheadings}{\normalfont\slshape\rightmark}{}{\normalfont{\thepage}}
\makerunningwidth{loveheadings}{\textwidth}
\makeheadrule{loveheadings}{\textwidth}{0pt} % \normalrulethickness
    \makepsmarks{loveheadings}{%
      \let\@mkboth\markboth
      \def\chaptermark##1{%
        \markboth{{%
          \ifnum \c@secnumdepth >\m@ne
            \if@mainmatter
              \strut\@chapapp\ \thechapter. \thinspace
            \fi
          \fi
          ##1}}{}}%
      \def\tocmark{\markboth{{\contentsname}}{}}%
      \def\lofmark{\markboth{{\listfigurename}}{}}%
      \def\lotmark{\markboth{{\listtablename}}{}}%
      \def\bibmark{\markboth{{\bibname}}{}}%
      \def\indexmark{\markboth{{\indexname}}{}}%
      \def\sectionmark##1{%
        \markright{{%
          \ifnum \c@secnumdepth > \z@
            \strut\thesection. \thinspace
          \fi
          ##1}}}%
    }
\pagestyle{loveheadings}

%% Strikethrough

\newcommand{\soutthick}[1]{%
    \renewcommand{\ULthickness}{.8pt}%
       \sout{#1}%
    \renewcommand{\ULthickness}{.4pt}% Resetting to ulem default
}

%% Math symbols

%% TYPESETTING
\renewcommand\Longrightarrow{\mathrel{{{\color{black}\Rightarrow}\kern-1.1ex\lower.1ex\hbox{\rlap{\color{white}\ensuremath{\blacksquare}}}\kern-0.9ex}\joinrel{\color{black}\Rightarrow}}}

\let\oldneq=\neq
\renewcommand\neq{\hbox{\mathversion{normal}\ensuremath{\oldneq}}}

%% Bullets

\newcommand{\localtextbulletone}{\textcolor{black}{\raisebox{.375ex}{\rule{.6ex}{.6ex}}}}
\renewcommand{\labelitemi}{\localtextbulletone}

%% Pieces of text

\newcommand\mathlibcommunity{The \texttt{mathlib} Community}
\newcommand\raamsdonk{van Raamsdonk}

\newcommand\thekeyidea[1]{%
The key idea is that the {#1} should be syntactically correct at all times. The
only red underlining we should see in Visual Studio Code should appear under
the placeholders. In general, a good principle for software development is to
start with a program that compiles, perform the smallest change possible to
obtain a new compiling program, and repeat until the program is complete.%
}

%% Quoting

\newenvironment{quotecode}
 {\list{}{\leftmargin\parindent}%
  \item\relax}
 {\endlist}

%% More tablet-specific layout

\ifdefined\TABLET
  \def\lstleftmargin{0em}
  \def\lstrightmargin{-1em}
  \setlength\footskip{1.5\baselineskip}
  \setlength\parindent{1.5em}
  \prfinterspace=1em
  \def\lstsize{\small}
  \def\summarysize{\footnotesize}
  \def\tabletsmall{\small}
  \def\tabletfootnotesize{\footnotesize}
  \def\tablettiny{\tiny}
  \def\tabletbreak#1{\\\noindent\hbox{}#1}
  \def\edition{Tablet}
  \renewenvironment{quote}{%
      \list{}{\leftmargin0pt\rightmargin\leftmargin}%
      \item\relax}
    {\endlist}
  \renewenvironment{quotecode}{%
      \list{}{\leftmargin0pt\rightmargin\leftmargin}%
      \item\relax}
    {\endlist}
\else
  \def\lstleftmargin{\leftmargin}
  \def\lstrightmargin{0pt}
  \def\lstsize{\normalsize}
  \def\summarysize{\small}
  \let\tabletsmall=\relax
  \let\tabletfootnotesize=\relax
  \let\tablettiny=\relax
  \def\tabletbreak#1{}
  \def\edition{Standard}
\fi

%% Lean code

\def\lstlanguagefiles{lstleanx.sty,lstleanxbw.sty,lstminijavaandc.sty}

\renewcommand\lst@visiblespace{\ensuremath{\;}}
\newcommand\li{\lstinline[language=leanxbw,showspaces=true]}
\newcommand\lic{\lstinline[language=leanx,showspaces=true]}
\newcommand\licw{\lstinline[language=leanx]}

\lstset{
  language=leanx,
  basicstyle=\ttfamily\lstsize,
  xleftmargin=\lstleftmargin,
  xrightmargin=\lstrightmargin,
  includerangemarker=false,
  rangebeginprefix=--quo\ ,
  rangeendprefix=--ou}

\definecolor{keywordcolor}{rgb}{0,0,1}          % blue
\definecolor{sortcolor}{rgb}{0,0,1}             % blue
\definecolor{commentcolor}{rgb}{0,0.5,0}        % darkish green
\definecolor{stringcolor}{rgb}{.65,.07,.04}     % reddish
\definecolor{symbolcolor}{rgb}{.18,.49,.72}     % blueish
\definecolor{sorrycolor}{rgb}{0.91,0,0}         % fairly hot red
\definecolor{numeralcolor}{rgb}{0,0.53,0.34}    % greenish
\definecolor{modifiercolor}{rgb}{.69,0,.87}     % magentaish
\definecolor{procnamecolor}{rgb}{.55,.37,.13}   % brownish
\definecolor{ctxtcolor}{rgb}{.85,.46,0}         % orange
\definecolor{preprocessorcolor}{rgb}{0,0,1}     % blue

\newcommand\ctxt[1]{{\ttfamily\bfseries\color{ctxtcolor}#1}}
\newcommand\ttvar[1]{\text{\ttfamily\slshape#1}}

\newcommand\mathscr[1]{\mathcal{#1}}
