Fix list append.

2 files changed, 8 insertions, 4 deletions

diff --git a/main.tex b/main.tex
index 911399f..7a82b2b 100644
--- a/main.tex
+++ b/main.tex
@@ -165,6 +165,9 @@
 \newcommand\judgement[4][]{{#2} \vdash^{#1} {#3} : {#4}}
 \newcommand\jdgmnt[3]{{#2} \vdash {#3}~\mathrm{#1}}
 
+% List operators
+\newcommand\append{\mathbin{@}}
+
 %%% Term syntax
 
 %% Let
diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index b697150..b93ca8f 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -491,10 +491,11 @@ At this point, the only type former 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 types \(A_i\) in
-argument form, their union is the concatenation \(A_1 ++ A_2 ++ \cdots ++
-A_n\). To inject type \(A_k\) into the union, we ignore the function
-arguments for all the other type constructors. To project type \(A_k\)
-out of the union, we pass \(\mathsf{arb}\) to all the other arguments.
+argument form, their union is the concatenation \(A_1 \append A_2
+\append \cdots \append A_n\). To inject type \(A_k\) into the union, we
+ignore the function arguments for all the other type constructors. To
+project type \(A_k\) out of the union, we pass \(\mathsf{arb}\) to all
+the other arguments.
 
 Using this argument-form union, we remove the need to perform
 induction on types, and only have to iterate over the number of types