summaryrefslogtreecommitdiff
path: root/sec/lang.ltx
diff options
context:
space:
mode:
authorChloe Brown <chloe.brown.00@outlook.com>2025-05-06 16:00:11 +0100
committerChloe Brown <chloe.brown.00@outlook.com>2025-05-06 16:00:11 +0100
commitde463fdc28ca9e32627818f508509d870c8a948b (patch)
treedc9ff5da85b3f31d40c011c6d2129e6946f19cb2 /sec/lang.ltx
parent27d17d272cb291ca3838565bb0f1c2dfbe630983 (diff)
Change signature of `\casetm`.
Diffstat (limited to 'sec/lang.ltx')
-rw-r--r--sec/lang.ltx6
1 files changed, 3 insertions, 3 deletions
diff --git a/sec/lang.ltx b/sec/lang.ltx
index 3b0134a..1ad22d4 100644
--- a/sec/lang.ltx
+++ b/sec/lang.ltx
@@ -104,7 +104,7 @@ unrepresentable in some models of System~T}.
\begin{prooftree}
\hypo{\judgement{\Gamma}{t}{\sum_i A_i}}
\hypo{\rangeover{\judgement{\Gamma, x_i : A_i}{t_i}{B}}{i}}
- \infer2{\judgement{\Gamma}{\casetm{t}{x_i}{t_i}{i}}{B}}
+ \infer2{\judgement{\Gamma}{\casetm{t}{\tuple{i,x_i}}{t_i}{i}}{B}}
\end{prooftree}
\\\\
\multicolumn{2}{c}{
@@ -156,7 +156,7 @@ derivation \(\jdgmnt{ty}{\Psi}{A}\), with our chosen variable \(X \in \Psi\).
\maptm{X}{A \to B} &\coloneq \lambda f, x. x \\
\maptm{X}{\prod_i A_i} &\coloneq \lambda f, x. \tuple{\rangeover{\maptm{X}{A_i}~f~x.i}{i}} \\
\maptm{X}{\sum_i A_i} &\coloneq
- \lambda f, x. \casetm{x}{x_i}{\tuple{i, \maptm{X}{A_i}~f~x_i}}{i} \\
+ \lambda f, x. \casetm{x}{\tuple{i,x_i}}{\tuple{i, \maptm{X}{A_i}~f~x_i}}{i} \\
\maptm{X}{\mu Y. A} &\coloneq
\lambda f, x.
\dofold{x}{y}{\roll~(\maptm{X}{\sub{A}{Y/\mu Y. \sub{A}{X/C}}}~f~y)}
@@ -193,7 +193,7 @@ do not accidentally depend on an equation that does not hold.
\begin{align*}
(\lambda x. t)~u &\coloneq \sub{t}{x/u}
&
- \casetm{\tuple{k, t}}{x_i}{u_i}{i} &\coloneq \sub{u_k}{x_k/t}
+ \casetm{\tuple{k, t}}{\tuple{i,x_i}}{u_i}{i} &\coloneq \sub{u_k}{x_k/t}
\\
\tuple{\rangeover{t_i}{i}}.k &\coloneq t_k
&