From f5338435ecbbf599efe5bca7c5205dd6d251deee Mon Sep 17 00:00:00 2001
From: Dan Licata <drl@cs.cmu.edu>
Date: Tue, 30 Oct 2018 01:01:41 -0400
Subject: [PATCH] minimize some of the running into the margin
---
paper/gtt.tex | 25 +++++++++++++------------
1 file changed, 13 insertions(+), 12 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 97c1240..64a670a 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1050,7 +1050,8 @@ orderings on types and terms.
\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 () \mid \pmpairWtoinZ V V' \\
- \mid (V_1,V_2) \mid \pmpairWtoXYinZ V x y V' \mid \thunk{M}
+ \mid (V_1,V_2) \mid \pmpairWtoXYinZ V x y V' \\
+ \mid \thunk{M}
\end{array} &
M,S ::= & \begin{array}{l}
@@ -1124,18 +1125,18 @@ orderings on types and terms.
\inferrule*[lab=$1$I]
{ }
{\Gamma \vdash (): 1}
- \qquad
+ \quad
\inferrule*[lab=$1$E]
{\Gamma \vdash V : 1 \and
\Gamma \mid \Delta \vdash E : T
}
{\Gamma \mid \Delta \vdash \pmpairWtoinZ V E : T}
- \qquad
+ \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}
- \qquad
+ \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
@@ -1145,15 +1146,15 @@ orderings on types and terms.
\inferrule*[lab=$U$I]
{\Gamma \mid \cdot \vdash M : \u B}
{\Gamma \vdash \thunk M : U \u B}
- \qquad
+ \quad
\inferrule*[lab=$U$E]
{\Gamma \vdash V : U \u B}
{\Gamma \pipe \cdot \vdash \force V : \u B}
- \qquad
+ \quad
\inferrule*[lab=$F$I]
{\Gamma \vdash V : A}
{\Gamma \pipe \cdot \vdash \ret V : \u F A}
- \qquad
+ \quad
\inferrule*[lab=$F$E]
{\Gamma \pipe \Delta \vdash M : \u F A \\
\Gamma, x: A \pipe \cdot \vdash N : \u B}
@@ -1162,7 +1163,7 @@ orderings on types and terms.
\inferrule*[lab=$\to$I]
{\Gamma, x: A \pipe \Delta \vdash M : \u B}
{\Gamma \pipe \Delta \vdash \lambda x : A . M : A \to \u B}
- \qquad
+ \quad
\inferrule*[lab=$\to$E]
{\Gamma \pipe \Delta \vdash M : A \to \u B\and
\Gamma \vdash V : A}
@@ -1170,16 +1171,16 @@ orderings on types and terms.
\iflong
\\\\
\inferrule*[lab=$\top$I]{ }{\Gamma \mid \Delta \vdash \emptypair : \top}
- \qquad
+ \quad
\inferrule*[lab=$\with$I]
{\Gamma \mid \Delta \vdash M_1 : \u B_1\and
\Gamma \mid \Delta \vdash M_2 : \u B_2}
{\Gamma \mid \Delta \vdash \pair {M_1} {M_2} : \u B_1 \with \u B_2}
- \qquad
+ \quad
\inferrule*[lab=$\with$E]
{\Gamma \mid \Delta \vdash M : \u B_1 \with \u B_2}
{\Gamma \mid \Delta \vdash \pi M : \u B_1}
- \qquad
+ \quad
\inferrule*[lab=$\with$E']
{\Gamma \mid \Delta \vdash M : \u B_1 \with \u B_2}
{\Gamma \mid \Delta \vdash \pi' M : \u B_2}
@@ -1735,7 +1736,7 @@ our design choice is forced for all casts, as long as the casts between ground t
{\Phi \vdash V_1 \ltdyn V_1' : A_1 \ltdyn A_1'\\\\
\Phi\vdash V_2 \ltdyn V_2' : A_2 \ltdyn A_2'}
{\Phi \vdash (V_1,V_2) \ltdyn (V_1',V_2') : A_1 \times A_2 \ltdyn A_1' \times A_2'}
- \qquad
+ \quad
\inferrule*[lab=$\times$ECong]
{\Phi \vdash V \ltdyn V' : A_1 \times A_2 \ltdyn A_1' \times A_2' \\\\
\Phi, x \ltdyn x' : A_1 \ltdyn A_1', y \ltdyn y' : A_2 \ltdyn A_2' \mid \Psi \vdash E \ltdyn E' : T \ltdyn T'
--
GitLab