From 0597f35602ad67113650de666c1e45ad1c125e5a Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Fri, 26 Oct 2018 11:22:14 -0400
Subject: [PATCH] make almost all of the named rules go above rather than on
the side
---
paper/gtt.tex | 98 +++++++++++++++++++++++++--------------------------
1 file changed, 49 insertions(+), 49 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index e14ed2c..b7d195f 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1063,42 +1063,42 @@ lemmas, and proofs.
\begin{array}{c}
\framebox{$\Gamma \vdash V : A$ and $\Gamma \mid \Delta \vdash M : \u B$} \qquad
\colorbox{lightgray}{
- $\inferrule*[right=UpCast]
+ $\inferrule*[lab=UpCast]
{\Gamma \vdash V : A \and A \ltdyn A'}
{\Gamma \vdash \upcast A {A'} V : A'}$
\qquad
- $\inferrule*[right=DnCast]
+ $\inferrule*[lab=DnCast]
{\Gamma\pipe \Delta \vdash M : \u B' \and \u B \ltdyn \u B'}
{\Gamma\pipe \Delta \vdash \dncast{\u B}{\u B'} M : \u B}$
}
\\\\
- \inferrule*[right=Var]
+ \inferrule*[lab=Var]
{ }
{\Gamma,x : A,\Gamma' \vdash x : A}
\qquad
- \inferrule*[right=Hole]
+ \inferrule*[lab=Hole]
{ }
{\Gamma\pipe \bullet : \u B \vdash \bullet : \u B}
\qquad
- \inferrule*[right=Err]
+ \inferrule*[lab=Err]
{ }
{\Gamma \mid \cdot \vdash \err_{\u B} : \u B}
\\
\iflong
\\
- \inferrule*[right=$0$E]
+ \inferrule*[lab=$0$E]
{\Gamma \vdash V : 0}
{\Gamma \mid \Delta \vdash \abort V : T}
\qquad
- \inferrule*[right=$+$Il]
+ \inferrule*[lab=$+$Il]
{\Gamma \vdash V : A_1}
{\Gamma \vdash \inl V : A_1 + A_2}
\qquad
- \inferrule*[right=$+$Ir]
+ \inferrule*[lab=$+$Ir]
{\Gamma \vdash V : A_2}
{\Gamma \vdash \inr V : A_1 + A_2}
\qquad
- \inferrule*[right=$+$E]
+ \inferrule*[lab=$+$E]
{
\Gamma \vdash V : A_1 + A_2 \\\\
\Gamma, x_1 : A_1 \mid \Delta \vdash E_1 : T \\\\
@@ -1107,66 +1107,66 @@ lemmas, and proofs.
{\Gamma \mid \Delta \vdash \caseofXthenYelseZ V {x_1. E_1}{x_2.E_2} : T}
\\\\
\fi
- \inferrule*[right=$1$I]
+ \inferrule*[lab=$1$I]
{ }
{\Gamma \vdash (): 1}
\qquad
- \inferrule*[right=$1$E]
+ \inferrule*[lab=$1$E]
{\Gamma \vdash V : 1 \and
\Gamma \mid \Delta \vdash E : T
}
{\Gamma \mid \Delta \vdash \pmpairWtoinZ V E : T}
\qquad
- \inferrule*[right=$\times$I]
+ \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
- \inferrule*[right=$\times$E]
+ \inferrule*[lab=$\times$E]
{\Gamma \vdash V : A_1 \times A_2 \\\\
\Gamma, x : A_1,y : A_2 \mid \Delta \vdash E : T
}
{\Gamma \mid \Delta \vdash \pmpairWtoXYinZ V x y E : T}
\\\\
- \inferrule*[right=$U$I]
+ \inferrule*[lab=$U$I]
{\Gamma \mid \cdot \vdash M : \u B}
{\Gamma \vdash \thunk M : U \u B}
\qquad
- \inferrule*[right=$U$E]
+ \inferrule*[lab=$U$E]
{\Gamma \vdash V : U \u B}
{\Gamma \pipe \cdot \vdash \force V : \u B}
\qquad
- \inferrule*[right=$F$I]
+ \inferrule*[lab=$F$I]
{\Gamma \vdash V : A}
{\Gamma \pipe \cdot \vdash \ret V : \u F A}
\qquad
- \inferrule*[right=$F$E]
+ \inferrule*[lab=$F$E]
{\Gamma \pipe \Delta \vdash M : \u F A \\
\Gamma, x: A \pipe \cdot \vdash N : \u B}
{\Gamma \pipe \Delta \vdash \bindXtoYinZ M x N : \u B}
\\\\
- \inferrule*[right=$\to$I]
+ \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
- \inferrule*[right=$\to$E]
+ \inferrule*[lab=$\to$E]
{\Gamma \pipe \Delta \vdash M : A \to \u B\and
\Gamma \vdash V : A}
{\Gamma \pipe \Delta \vdash M\,V : \u B }
\iflong
\\\\
- \inferrule*[right=$\top$I]{ }{\Gamma \mid \Delta \vdash \emptypair : \top}
+ \inferrule*[lab=$\top$I]{ }{\Gamma \mid \Delta \vdash \emptypair : \top}
\qquad
- \inferrule*[right=$\with$I]
+ \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
- \inferrule*[right=$\with$E]
+ \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
- \inferrule*[right=$\with$E']
+ \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}
\fi
@@ -1657,43 +1657,43 @@ types and the dynamic types have this property.
\framebox{$\Phi \vdash V \ltdyn V' : A \ltdyn A'$ and $\Phi \mid \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'$}
\\\\
- \inferrule*[right=TmDynRefl]{ }{\Gamma \ltdyn \Gamma \mid \Delta \ltdyn \Delta \vdash E \ltdyn E : T \ltdyn T}
+ \inferrule*[lab=TmDynRefl]{ }{\Gamma \ltdyn \Gamma \mid \Delta \ltdyn \Delta \vdash E \ltdyn E : T \ltdyn T}
\qquad
- \inferrule*[right=TmDynTrans]{\Gamma \ltdyn \Gamma' \mid \Delta \ltdyn \Delta' \vdash E \ltdyn E' : T \ltdyn T' \\\\
+ \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*[right=TmDynVar]
+ \inferrule*[lab=TmDynVar]
{ }
{\Phi,x \ltdyn x' : A \ltdyn A',\Phi' \vdash x \ltdyn x' : A \ltdyn A'}
\qquad
- \inferrule*[right=TmDynValSubst]
+ \inferrule*[lab=TmDynValSubst]
{\Phi \vdash V \ltdyn V' : A \ltdyn A' \\\\
\Phi, x \ltdyn x' : A \ltdyn A',\Phi' \pipe \Psi \vdash E \ltdyn E' : T \ltdyn T'
}
{\Phi \mid \Psi \vdash E[V/x] \ltdyn E'[V'/x'] : T \ltdyn T'}
\\\\
- \inferrule*[right=TmDynHole]
+ \inferrule*[lab=TmDynHole]
{ }
{\Phi \pipe \bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn \bullet : \u B \ltdyn \u B'}
\qquad
- \inferrule*[right=TmDynStkSubst]
+ \inferrule*[lab=TmDynStkSubst]
{\Phi \pipe \Psi \vdash M_1 \ltdyn M_1' : \u B_1 \ltdyn \u B_1' \\\\
\Phi \pipe \bullet \ltdyn \bullet : \u B_1 \ltdyn \u B_1' \vdash M_2 \ltdyn M_2' : \u B_2 \ltdyn \u B_2'
}
{\Phi \mid \Psi \vdash M_2[M_1/\bullet] \ltdyn M_2'[M_1'/\bullet] : \u B_2 \ltdyn \u B_2'}
\\\\
\iflong
- \inferrule*[right=$+$IlCong]
+ \inferrule*[lab=$+$IlCong]
{\Phi \vdash V \ltdyn V' : A_1 \ltdyn A_1'}
{\Phi \vdash \inl V \ltdyn \inl V' : A_1 + A_2 \ltdyn A_1' + A_2'}
\qquad
- \inferrule*[right=$+$IrCong]
+ \inferrule*[lab=$+$IrCong]
{\Phi \vdash V \ltdyn V' : A_2 \ltdyn A_2'}
{\Phi \vdash \inr V \ltdyn \inr V' : A_1 + A_2 \ltdyn A_1' + A_2'}
\\\\
- \inferrule*[right=$+$ECong]
+ \inferrule*[lab=$+$ECong]
{
\Phi \vdash V \ltdyn V' : A_1 + A_2 \ltdyn A_1' + A_2' \\\\
\Phi, x_1 \ltdyn x_1' : A_1 \ltdyn A_1' \mid \Psi \vdash E_1 \ltdyn E_1' : T \ltdyn T' \\\\
@@ -1701,71 +1701,71 @@ types and the dynamic types have this property.
}
{\Phi \mid \Psi \vdash \caseofXthenYelseZ V {x_1. E_1}{x_2.E_2} \ltdyn \caseofXthenYelseZ V {x_1'. E_1'}{x_2'.E_2'} : T'}
\qquad
- \inferrule*[right=$0$ECong]
+ \inferrule*[lab=$0$ECong]
{\Phi \vdash V \ltdyn V' : 0 \ltdyn 0}
{\Phi \mid \Psi \vdash \abort V \ltdyn \abort V' : T \ltdyn T'}
\\\\
- \inferrule*[right=$1$ICong]{ }{\Phi \vdash () \ltdyn () : 1 \ltdyn 1}
+ \inferrule*[lab=$1$ICong]{ }{\Phi \vdash () \ltdyn () : 1 \ltdyn 1}
\qquad
- \inferrule*[right=$1$ECong]
+ \inferrule*[lab=$1$ECong]
{\Phi \vdash V \ltdyn V' : 1 \ltdyn 1 \\\\
\Phi \mid \Psi \vdash E \ltdyn E' : T \ltdyn T'
}
{\Phi \mid \Psi \vdash \pmpairWtoinZ V E \ltdyn \pmpairWtoinZ V' E' : T \ltdyn T'}
\\\\
\fi
- \inferrule*[right=$\times$ICong]
+ \inferrule*[lab=$\times$ICong]
{\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
- \inferrule*[right=$\times$ECong]
+ \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'
}
{\Phi \mid \Psi \vdash \pmpairWtoXYinZ V x y E \ltdyn \pmpairWtoXYinZ {V'} {x'} {y'} {E'} : T \ltdyn T'}
\\\\
\iflong
- \inferrule*[right=$U$ICong]
+ \inferrule*[lab=$U$ICong]
{\Phi \mid \cdot \vdash M \ltdyn M' : \u B \ltdyn \u B'}
{\Phi \vdash \thunk M \ltdyn \thunk M' : U \u B \ltdyn U \u B'}
\qquad
- \inferrule*[right=$U$ECong]
+ \inferrule*[lab=$U$ECong]
{\Phi \vdash V \ltdyn V' : U \u B \ltdyn U \u B'}
{\Phi \pipe \cdot \vdash \force V \ltdyn \force V' : \u B \ltdyn \u B'}
\\\\
\fi
- \inferrule*[right=$F$ICong]
+ \inferrule*[lab=$F$ICong]
{\Phi \vdash V \ltdyn V' : A \ltdyn A'}
{\Phi \pipe \cdot \vdash \ret V \ltdyn \ret V' : \u F A \ltdyn \u F A'}
\qquad
- \inferrule*[right=$F$ECong]
+ \inferrule*[lab=$F$ECong]
{\Phi \pipe \Psi \vdash M \ltdyn M' : \u F A \ltdyn \u F A' \\\\
\Phi, x \ltdyn x' : A \ltdyn A' \pipe \cdot \vdash N \ltdyn N' : \u B \ltdyn \u B'}
{\Phi \pipe \Psi \vdash \bindXtoYinZ M x N \ltdyn \bindXtoYinZ {M'} {x'} {N'} : \u B \ltdyn \u B'}
\\\\
- \inferrule*[right=$\to$ICong]
+ \inferrule*[lab=$\to$ICong]
{\Phi, x \ltdyn x' : A \ltdyn A' \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'}
{\Phi \pipe \Psi \vdash \lambda x : A . M \ltdyn \lambda x' : A' . M' : A \to \u B \ltdyn A' \to \u B'}
\qquad
- \inferrule*[right=$\to$ECong]
+ \inferrule*[lab=$\to$ECong]
{\Phi \pipe \Psi \vdash M \ltdyn M' : A \to \u B \ltdyn A' \to \u B' \\\\
\Phi \vdash V \ltdyn V' : A \ltdyn A'}
{\Phi \pipe \Psi \vdash M\,V \ltdyn M'\,V' : \u B \ltdyn \u B' }
\\\\
\iflong
- \inferrule*[right=$\top$ICong]{ }{\Phi \mid \Psi \vdash \{\} \ltdyn \{\} : \top \ltdyn \top}
+ \inferrule*[lab=$\top$ICong]{ }{\Phi \mid \Psi \vdash \{\} \ltdyn \{\} : \top \ltdyn \top}
\qquad
- \inferrule*[right=$\with$ICong]
+ \inferrule*[lab=$\with$ICong]
{\Phi \mid \Psi \vdash M_1 \ltdyn M_1' : \u B_1 \ltdyn \u B_1'\and
\Phi \mid \Psi \vdash M_2 \ltdyn M_2' : \u B_2 \ltdyn \u B_2'}
{\Phi \mid \Psi \vdash \pair {M_1} {M_2} \ltdyn \pair {M_1'} {M_2'} : \u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
\\\\
- \inferrule*[right=$\with$ECong]
+ \inferrule*[lab=$\with$ECong]
{\Phi \mid \Psi \vdash M \ltdyn M' : \u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
{\Phi \mid \Psi \vdash \pi M \ltdyn \pi M' : \u B_1 \ltdyn \u B_1'}
\qquad
- \inferrule*[right=$\with$E'Cong]
+ \inferrule*[lab=$\with$E'Cong]
{\Phi \mid \Psi \vdash M \ltdyn M' : \u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
{\Phi \mid \Psi \vdash \pi' M \ltdyn \pi' M' : \u B_2 \ltdyn \u B_2'}
\fi
@@ -2014,10 +2014,10 @@ heterogeneous way, which includes congruence $\Gamma \ltdyn \Gamma'
\begin{mathpar}
\framebox{Error Properties}
\qquad
- \inferrule*[right=ErrBot]{ \Gamma' \mid \cdot \vdash M' : \u B' }
+ \inferrule*[lab=ErrBot]{ \Gamma' \mid \cdot \vdash M' : \u B' }
{ \Gamma \ltdyn \Gamma' \mid \cdot \vdash \err \ltdyn M' : \u B \ltdyn \u B'}
\qquad
- \inferrule*[right=StkStrict] { \Gamma \mid x : \u B \vdash S : \u B'}
+ \inferrule*[lab=StkStrict] { \Gamma \mid x : \u B \vdash S : \u B'}
{\Gamma \mid \cdot \vdash S[\err_{\u B}] \ltdyn \err_{\u{B'}} : \u B'}
\end{mathpar}
\end{small}
--
GitLab