From a28b3c5b659ae350c033374a9c8737dc6d314f75 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Mon, 29 Oct 2018 18:30:28 -0400
Subject: [PATCH] save some space on figures
---
paper/gtt.tex | 32 ++++++++++++++++----------------
1 file changed, 16 insertions(+), 16 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 6be5cb1..044730c 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1487,35 +1487,35 @@ domain~\cite{newahmed18,newlicata2018-fscd}.
\begin{mathpar}
\framebox{$A \ltdyn A'$ and $\u B \ltdyn \u B'$}
- \inferrule*[right=VTyRefl]{ }{A \ltdyn A}
+ \inferrule*[lab=VTyRefl]{ }{A \ltdyn A}
- \inferrule*[right=VTyTrans]{A \ltdyn A' \and A' \ltdyn A''}
+ \inferrule*[lab=VTyTrans]{A \ltdyn A' \and A' \ltdyn A''}
{A \ltdyn A''}
- \inferrule*[right=CTyRefl]{ }{\u B \ltdyn \u B'}
+ \inferrule*[lab=CTyRefl]{ }{\u B \ltdyn \u B'}
- \inferrule*[right=CTyTrans]{\u B \ltdyn \u B' \and \u B' \ltdyn \u B''}
+ \inferrule*[lab=CTyTrans]{\u B \ltdyn \u B' \and \u B' \ltdyn \u B''}
{\u B \ltdyn \u B''}
- \inferrule*[right=VTyTop]{ }{A \ltdyn \dynv}
+ \inferrule*[lab=VTyTop]{ }{A \ltdyn \dynv}
- \inferrule*[right=$U$Mon]{\u B \ltdyn \u B'}
+ \inferrule*[lab=$U$Mon]{\u B \ltdyn \u B'}
{U B \ltdyn U B'}
- \inferrule*[right=$+$Mon]{A_1 \ltdyn A_1' \and A_2 \ltdyn A_2' }
+ \inferrule*[lab=$+$Mon]{A_1 \ltdyn A_1' \and A_2 \ltdyn A_2' }
{A_1 + A_2 \ltdyn A_1' + A_2'}
- \inferrule*[right=$\times$Mon]{A_1 \ltdyn A_1' \and A_2 \ltdyn A_2' }
+ \inferrule*[lab=$\times$Mon]{A_1 \ltdyn A_1' \and A_2 \ltdyn A_2' }
{A_1 \times A_2 \ltdyn A_1' \times A_2'}
\\
- \inferrule*[right=CTyTop]{ }{\u B \ltdyn \dync}
+ \inferrule*[lab=CTyTop]{ }{\u B \ltdyn \dync}
-\inferrule*[right=$F$Mon]{A \ltdyn A' }{ \u F A \ltdyn \u F A'}
+\inferrule*[lab=$F$Mon]{A \ltdyn A' }{ \u F A \ltdyn \u F A'}
-\inferrule*[right=$\with$Mon]{\u B_1 \ltdyn \u B_1' \and \u B_2 \ltdyn \u B_2'}
+\inferrule*[lab=$\with$Mon]{\u B_1 \ltdyn \u B_1' \and \u B_2 \ltdyn \u B_2'}
{\u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
-\inferrule*[right=$\to$Mon]{A \ltdyn A' \and \u B \ltdyn \u B'}
+\inferrule*[lab=$\to$Mon]{A \ltdyn A' \and \u B \ltdyn \u B'}
{A \to \u B \ltdyn A' \to \u B'}
\begin{longonly}
\\
@@ -1664,14 +1664,14 @@ our design choice is forced for all casts, as long as the casts between ground t
\inferrule*[lab=TmDynRefl]{ }{\Gamma \ltdyn \Gamma \mid \Delta \ltdyn \Delta \vdash E \ltdyn E : T \ltdyn T}
\qquad
+ \inferrule*[lab=TmDynVar]
+ { }
+ {\Phi,x \ltdyn x' : A \ltdyn A',\Phi' \vdash x \ltdyn x' : A \ltdyn A'}
+ \\\\
\inferrule*[lab=TmDynTrans]{\Gamma \ltdyn \Gamma' \mid \Delta \ltdyn \Delta' \vdash E \ltdyn E' : T \ltdyn T' \\\\
\Gamma' \ltdyn \Gamma'' \mid \Delta' \ltdyn \Delta'' \vdash E' \ltdyn E'' : T' \ltdyn T''
}
{\Gamma \ltdyn \Gamma'' \mid \Delta \ltdyn \Delta'' \vdash E \ltdyn E'' : T \ltdyn T''}
- \\\\
- \inferrule*[lab=TmDynVar]
- { }
- {\Phi,x \ltdyn x' : A \ltdyn A',\Phi' \vdash x \ltdyn x' : A \ltdyn A'}
\qquad
\inferrule*[lab=TmDynValSubst]
{\Phi \vdash V \ltdyn V' : A \ltdyn A' \\\\
--
GitLab