diff options
| -rw-r--r-- | sec/encoding.ltx | 6 |
1 files changed, 3 insertions, 3 deletions
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 |