From 7b38cbcde83ba18f3c594ee64ffa857e07b7829f Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 6 May 2025 16:00:32 +0100
Subject: Justify encoding sum as tagged union.

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

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index cd749a9..b27f9d5 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -373,9 +373,16 @@ Unions have two operators: \(\mathsf{inj}~i~t\) and
 have the beta reduction rule \(\mathsf{prj}~(\mathsf{inj}~i~t)~i =
 t\). If the two type indices are different then projection is stuck.
 
+We encode the injection into a sum \(\tuple{i, t}\) by the pair
+\(\tuple{i, \mathsf{inj}~i~t}\). We encode pattern matching
+\((\casetm{t}{\tuple{i,x_i}}{t_i}{i})\) by the term \(
+(\casetm{t.0}{i}{\sub{t_i}{x_i/\mathsf{prj}~t.1~i}}{i})
+\) performing a pattern match over the tag to find the correct branch
+to take. The pattern match on the right will be desugared into a
+sequence of equality tests in phase seven.
+
 \TODO{
   \begin{itemize}
-    \item justify why sums are tagged unions
     \item justify adding union types
     \item justify the case operator on naturals
   \end{itemize}
-- 
cgit v1.2.3