diff options
| -rw-r--r-- | main.tex | 2 | ||||
| -rw-r--r-- | sec/lang.ltx | 6 |
2 files changed, 4 insertions, 4 deletions
@@ -287,7 +287,7 @@ %% Sums \newcommand\matchtm[2]{\mathsf{match}~{#1}~\mathsf{with}~{#2}} -\newcommand\casetm[4]{\matchtm{#1}{\rangeover{\tuple{{#4}, {#2}}.~{#3}}{#4}}} +\newcommand\casetm[4]{\matchtm{#1}{\rangeover{{#2}.~{#3}}{#4}}} \ExplSyntaxOn \NewDocumentCommand \squid_matchpart:nn {m m m} 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 & |