formalism: Add mechanization indicators for each section

formalism/marked.tex

@@ -13,6 +13,11 @@ \section{Marked lambda calculus}
 numbers, booleans, and product types. Typed holes (written $\EEHole$) are included to model
 incomplete editor states \`a la Hazelnut but are not essential.
 
+\begin{mechanization}
+  \item core.agda
+  \item marking.agda
+\end{mechanization}
+
 \subsection{Syntax}
 \label{sec:marked-syntax}
 \[\begin{array}{rrcl}

formalism/patterned.tex

@@ -9,6 +9,8 @@
 \section{Extension: patterned let expressions}
 \label{sec:patterned}
 
+\nomechanization{}
+
 \subsection{Syntax}
 \label{sec:patterned-syntax}
 \[\begin{array}{rrcl}

formalism/polymorphism.tex

@@ -16,6 +16,8 @@ \section{Extension: System F-style polymorphism}
 (alongside extensions of the original consistency, etc. judgments) and linked by a marking
 operation.
 
+\nomechanization{}
+
 \subsection{Syntax}
 \label{sec:polymorphism-syntax}
 The syntax of unmarked types is exactly that of the original types alongside additional forms for

formalism/preamble/preamble.tex

@@ -18,6 +18,7 @@
 
 % font
 \usepackage{iftex}
+\usepackage{fontspec}
 \ifPDFTeX
   \usepackage{libertinust1math}
   \usepackage{libertine}
@@ -32,6 +33,9 @@
 \usepackage{relsize}
 \usepackage{centernot}
 
+% no indentation
+\usepackage{parskip}
+
 % hyperlinks
 \usepackage[colorlinks=true, linkcolor=purple]{hyperref}
 \usepackage[capitalise, noabbrev]{cleveref}
@@ -60,3 +64,15 @@
 
 % utilities
 \input{preamble/utilities}
+
+% mechanization notices
+\newenvironment{mechanization}{
+  \textsc{Mechanization} $\bm{\bigcirc}$
+  %
+  \begin{itemize}[label=$\blacktriangleright$, noitemsep]
+    \ttfamily
+}{
+  \end{itemize}
+}
+
+\newcommand{\nomechanization}{\textsc{Mechanization} $\times$}

formalism/typed.tex

@@ -10,6 +10,8 @@
 \section{Typed hazelnut}
 \label{sec:typed}
 
+\nomechanization{}
+
 \subsection{Syntax}
 \label{sec:typed-syntax}
 Zippered types are the same as in the untyped model.

formalism/untyped.tex

@@ -8,6 +8,10 @@
 \section{Untyped hazelnut}
 \label{sec:untyped}
 
+\begin{mechanization}
+  \item hazelnut.agda
+\end{mechanization}
+
 \subsection{Syntax}
 \label{sec:untyped-syntax}
 \[\begin{array}{rrcl}