diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-26 15:11:29 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-26 15:11:29 +0100 |
| commit | 2eaa70248abba984b17a422855406c28c9076bf4 (patch) | |
| tree | ee8ffa53e72cd54b5fe80283cd3339e54469e4dc /sec | |
| parent | c6281fb177dd6794ed88a7f4e5c956eac0bea66a (diff) | |
Fix 721--727.
Diffstat (limited to 'sec')
| -rw-r--r-- | sec/encoding.ltx | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index c87ce90..fa40ec0 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -494,7 +494,7 @@ let dupfirst t = fun x => match x with \subsection{Phase 6: Encoding Unions}% \label{subsec:unions} -At this point, the only type former we use that is not present in +At this phase the only type former we use that is not present in System~T is the union type.\@ \textcite{oleg} gives an inductive encoding for binary unions. We instead use an encoding for unions derived from the argument form of types. Given we have a family of |