diff options
| -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 |