From 6f254165950514ae2a5b44f6a00c358bf8b66741 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 30 Apr 2025 16:04:12 +0100 Subject: Add headings for each phase. --- sec/encoding.ltx | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 34f3ae0..2ecb8cc 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -235,6 +235,9 @@ let compose (depth, heap) = \vspace{-\baselineskip} \end{listing} +\subsection{Phase 3: Encoding Lists}% +\label{subsec:lists} + \TODO{ \begin{itemize} \item state that we encode lists using their eliminators @@ -246,6 +249,9 @@ let compose (depth, heap) = \end{itemize} } +\subsection{Phase 4: Encoding Sums}% +\label{subsec:sums} + \TODO{ \begin{itemize} \item state that we encode sums as tagged C-style unions @@ -256,6 +262,9 @@ let compose (depth, heap) = \end{itemize} } +\subsection{Phase 5: Encoding Products}% +\label{subsec:products} + \TODO{ \begin{itemize} \item state that we encode products as functions from naturals to unions @@ -264,6 +273,9 @@ let compose (depth, heap) = \end{itemize} } +\subsection{Phase 6: Encoding Unions}% +\label{subsec:unions} + \TODO{ \begin{itemize} \item state that we encode unions as functions with possibly unused @@ -274,6 +286,9 @@ let compose (depth, heap) = \end{itemize} } +\subsection{Phase 7: Desugaring}% +\label{subsec:desugar} + \TODO{ \begin{itemize} \item state that we desugar other operators last -- cgit v1.2.3