Justify encoding sum as tagged union.

1 files changed, 8 insertions, 1 deletions

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}