From 975ad15faf5286b2be7fff5acd1ed06f883e2100 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 6 May 2025 15:35:44 +0100
Subject: State we encode sums as tagged unions.

---
 sec/encoding.ltx | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'sec')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 5dbe00f..c7506db 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -361,9 +361,14 @@ let compose (depth, heap) =
 \subsection{Phase 4: Encoding Sums}%
 \label{subsec:sums}
 
+In this phase we remove sums from the language by encoding them as
+tagged C-style unions, following the work of \textcite{oleg}. We
+encode the type \(\sum_i A_i\) by the pair \(\nat \times \bigsqcup_i A_i\), of
+a tag indicating which case we are in, and a union which can contain
+a value from any case.
+
 \TODO{
   \begin{itemize}
-    \item state that we encode sums as tagged C-style unions
     \item explain the operations and equations of unions
     \item justify why sums are tagged unions
     \item justify adding union types
-- 
cgit v1.2.3