From 4c87fb529b16ff54c8246eb04925b388a3e74be4 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 9 Dec 2021 06:13:32 -0600
Subject: [PATCH] Restyling

---
 Makefile              |  2 +-
 main.tex              | 21 ++++++++++++++++-----
 src/Project/Cesk.agda |  2 +-
 3 files changed, 18 insertions(+), 7 deletions(-)

diff --git a/Makefile b/Makefile
index dbf612a..fef6f09 100644
--- a/Makefile
+++ b/Makefile
@@ -12,6 +12,6 @@ agda.sty: $(GENERATED_TEX)
 	cp gentex/agda.sty agda.sty
 
 watch:
-	watchexec -e agda,tex -- make main.pdf
+	watchexec -e agda,tex -- make --jobs=4 main.pdf
 
 .PHONY: watch
diff --git a/main.tex b/main.tex
index 8f54446..f4fd755 100644
--- a/main.tex
+++ b/main.tex
@@ -7,7 +7,7 @@
 \usepackage{newunicodechar}
 \usepackage{url}
 
-\usetheme{CambridgeUS}
+% \usetheme{CambridgeUS}
 \usecolortheme{lily}
 \setbeamercovered{transparent}
 
@@ -16,7 +16,8 @@
 
 \titlegraphic{
   \centering
-  \includegraphics[width=.3\textwidth,height=.5\textheight]{cesk.png}
+  \vspace{-1cm}
+  \includegraphics[width=.2\textwidth,height=.35\textheight]{cesk.png}
 }
 \title{First class continuations with CEK machines in Agda}
 \author{Michael Zhang}
@@ -24,7 +25,10 @@
 
 \begin{document}
 
-\frame{\titlepage}
+% \frame{\titlepage}
+\begin{frame}[t]\vspace{1cm}
+  \maketitle
+\end{frame}
 
 \section{Primer on CESK}
 
@@ -39,13 +43,20 @@
 \end{frame}
 
 \begin{frame}
-  \frametitle{How does it work?}
+  \frametitle{What are each of the components?}
 
   \begin{itemize}[<+->]
-    \item 
+    \item $C$ontrol is your current term.
+    \item $E$nvironment is a list of addresses.
+    \item $S$tore is a mapping of addresses to values.
+    \item $K$ont is what gets evaluated next.
   \end{itemize}
 \end{frame}
 
+\begin{frame}
+  \frametitle{What are continuations?}
+\end{frame}
+
 \begin{frame}
   \begin{tikzpicture}[
       roundnode/.style={circle, draw=green!60, fill=green!5, very thick, minimum size=7mm},
diff --git a/src/Project/Cesk.agda b/src/Project/Cesk.agda
index bc8b33e..bb3407d 100644
--- a/src/Project/Cesk.agda
+++ b/src/Project/Cesk.agda
@@ -63,4 +63,4 @@ exp =
   ((ƛ $ atomic $ suc $ ` zero) · ` zero)
 
 expRes+ : eval 7 exp ≡ (complete $ done $ (suc (suc (suc zero))))
-expRes+ = refl
\ No newline at end of file
+expRes+ = refl