Skip to content

Commit

Permalink
formalism: Add mechanization indicators for each section
Browse files Browse the repository at this point in the history
  • Loading branch information
mirryi committed Oct 10, 2023
1 parent f1701a7 commit 587a5e7
Showing 6 changed files with 31 additions and 0 deletions.
5 changes: 5 additions & 0 deletions formalism/marked.tex
Original file line number Diff line number Diff line change
@@ -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}
2 changes: 2 additions & 0 deletions formalism/patterned.tex
Original file line number Diff line number Diff line change
@@ -9,6 +9,8 @@
\section{Extension: patterned let expressions}
\label{sec:patterned}

\nomechanization{}

\subsection{Syntax}
\label{sec:patterned-syntax}
\[\begin{array}{rrcl}
2 changes: 2 additions & 0 deletions formalism/polymorphism.tex
Original file line number Diff line number Diff line change
@@ -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
16 changes: 16 additions & 0 deletions formalism/preamble/preamble.tex
Original file line number Diff line number Diff line change
@@ -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$}
2 changes: 2 additions & 0 deletions formalism/typed.tex
Original file line number Diff line number Diff line change
@@ -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.
4 changes: 4 additions & 0 deletions formalism/untyped.tex
Original file line number Diff line number Diff line change
@@ -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}

0 comments on commit 587a5e7

Please sign in to comment.