From de3138bfe231b3bcf052eec12216957b8e7a12ef Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 26 Jun 2025 14:49:17 +0100 Subject: Fix 653--655. --- sec/encoding.ltx | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'sec/encoding.ltx') diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 079027a..2d32f30 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -392,9 +392,9 @@ let compose' (depth, heap) = 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. +encode the type \(\sum_{\ell \in I} A_\ell\) by the pair \(\nat \times \bigsqcup_{\ell \in I} A_\ell\) +of a tag indicating the variant, and a union which can contain a value +from any variant. Unions have two operators: \(\mathsf{inj}~i~t\) and \(\mathsf{prj}~t~i\) for injecting and projecting values at type -- cgit v1.2.3