From 5c954d7726e2a2c40b2d426247334ec5ebb678e3 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 7 May 2025 15:09:15 +0100 Subject: Fix list append. --- main.tex | 3 +++ sec/encoding.ltx | 9 +++++---- 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 -- cgit v1.2.3