From 3ec5e02ecf0730219f5ed2122508b061f11cbda8 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Mon, 5 Nov 2018 15:32:36 -0500
Subject: [PATCH] a space hack
---
paper/gtt.tex | 25 +++++++++++++------------
1 file changed, 13 insertions(+), 12 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index e94420b..9efa093 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1036,14 +1036,14 @@ orderings on types and terms.
\begin{small}
\[
\begin{array}{l}
- %
\begin{array}{rl|rl}
A ::= & \colorbox{lightgray}{$\dynv$} \mid U \u B \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 &
\u B ::= & \colorbox{lightgray}{$\dync$} \mid \u F A \mid \top \mid \u B_1 \with \u B_2 \mid A \to \u B\\
V ::= & \begin{array}{l}
\colorbox{lightgray}{$\upcast A {A'} V$} \mid x \mid \abort{V} \\
- \mid \inl{V} \mid \inr{V} \mid \caseofXthenYelseZ V {x_1. V_1}{x_2.V_2} \\
+ \mid \inl{V} \mid \inr{V} \\
+ \mid \caseofXthenYelseZ V {x_1. V_1}{x_2.V_2} \\
\mid () \mid \pmpairWtoinZ V V' \\
\mid (V_1,V_2) \mid \pmpairWtoXYinZ V x y V' \\
\mid \thunk{M}
@@ -1052,10 +1052,11 @@ orderings on types and terms.
M,S ::= & \begin{array}{l}
\colorbox{lightgray}{$\dncast{\u B} {\u B'} M$} \mid \bullet \mid \err_{\u B} \\
\mid \abort{V} \mid \caseofXthenYelseZ V {x_1. M_1}{x_2.M_2}\\
- \mid \pmpairWtoinZ V M \mid \pmpairWtoXYinZ V x y M \\
- \mid \force{V} \mid \ret{V} \mid \bindXtoYinZ{M}{x}{N}\\
- \mid \lambda x:A.M \mid M\,V \\
- \mid \emptypair \mid \pair{M_1}{M_2} \mid \pi M \mid \pi' M
+ \mid \pmpairWtoinZ V M \mid\pmpairWtoXYinZ V x y M \\
+ \mid \force{V} \mid \ret{V} \mid \bindXtoYinZ{M}{x}{N}\\
+ \mid \lambda x:A.M \mid M\,V\\
+ \mid \emptypair \mid \pair{M_1}{M_2} \\
+ \mid \pi M \mid \pi' M
\end{array}\\
\Gamma ::= & \cdot \mid \Gamma, x : A &
@@ -1120,18 +1121,18 @@ orderings on types and terms.
\inferrule*[lab=$1$I]
{ }
{\Gamma \vdash (): 1}
- \quad
+ \,\,\,
\inferrule*[lab=$1$E]
{\Gamma \vdash V : 1 \and
\Gamma \mid \Delta \vdash E : T
}
{\Gamma \mid \Delta \vdash \pmpairWtoinZ V E : T}
- \quad
+ \,\,\,
\inferrule*[lab=$\times$I]
{\Gamma \vdash V_1 : A_1\and
\Gamma\vdash V_2 : A_2}
{\Gamma \vdash (V_1,V_2) : A_1 \times A_2}
- \quad
+ \,\,\,
\inferrule*[lab=$\times$E]
{\Gamma \vdash V : A_1 \times A_2 \\\\
\Gamma, x : A_1,y : A_2 \mid \Delta \vdash E : T
@@ -1141,15 +1142,15 @@ orderings on types and terms.
\inferrule*[lab=$U$I]
{\Gamma \mid \cdot \vdash M : \u B}
{\Gamma \vdash \thunk M : U \u B}
- \quad
+ \,\,\,
\inferrule*[lab=$U$E]
{\Gamma \vdash V : U \u B}
{\Gamma \pipe \cdot \vdash \force V : \u B}
- \quad
+ \,\,\,
\inferrule*[lab=$F$I]
{\Gamma \vdash V : A}
{\Gamma \pipe \cdot \vdash \ret V : \u F A}
- \quad
+ \,\,\,
\inferrule*[lab=$F$E]
{\Gamma \pipe \Delta \vdash M : \u F A \\
\Gamma, x: A \pipe \cdot \vdash N : \u B}
--
GitLab