space

refining.tex

@@ -58,7 +58,7 @@ the set that contains the types of all the occurrences of $x$ in $e$. This
 judgement can be deduced by the following deduction system
 that collects type information on the variables that are $\lambda$-abstracted
 (i.e., those in the domain of $\Gamma$, since lambdas are our only
-binders):\vspace{-1mm}
+binders):\vspace{-1.5mm}
 \begin{mathpar}
 \Infer[Var]
     {
@@ -119,17 +119,17 @@ Where $\psi\setminus\{x\}$ is the function defined as $\psi$ but undefined on $x
 \noindent
 \else.~\fi
 All that remains to do is replace the rule [{\sc Abs}+] with the
-following rule\vspace{-1mm}
+following rule\vspace{-.8mm}
 \begin{mathpar}
   \Infer[AbsInf+]
   {\Gamma,x:s\vdash e\triangleright\psi
     \and
     \Gamma,x:s\vdash e:t
     \and
-    T = \{ (s,t) \} \cup \{ (u,v) ~|~
-      u\in\psi(x) \land \Gamma,x:u\vdash e:v \}}
+    T = \{ (s,t) \} \cup \{ (u,w) ~|~
+      u\in\psi(x) \land \Gamma,x:u\vdash e:w \}}
     {
-    \Gamma\vdash\lambda x:s.e:\textstyle\bigwedge_{(u,v) \in T}u\to v
+    \Gamma\vdash\lambda x:s.e:\textstyle\bigwedge_{(u,w) \in T}u\to w
     }
     {}\vspace{-2.5mm}
   \end{mathpar}
@@ -151,7 +151,7 @@ will be checked for the input types $\Int$, $\Real\setminus\Int$, and
 \Bool, yielding the expected result.
 
 It is not too difficult to generalize this rule when the lambda is
-typed by an intersection type:\vspace{-1mm}
+typed by an intersection type:\vspace{-.8mm}
 \begin{mathpar}
   \Infer[AbsInf+] {\forall i\in I~\Gamma,x:s_i\vdash
     e\triangleright\psi_i
@@ -159,10 +159,10 @@ typed by an intersection type:\vspace{-1mm}
     \Gamma,x:s_i\vdash
     e : t_i
     \and
-    T_i = \{ (u, v) ~|~ u\in\psi_i(x) \land \Gamma, x:u\vdash e : v\}
+    T_i = \{ (u, w) ~|~ u\in\psi_i(x) \land \Gamma, x:u\vdash e : w\}
   } {\textstyle \Gamma\vdash\lambda^{\bigwedge_{i\in
         I}s_i\to t_i} x.e:\bigwedge_{i\in I}(s_i\to
-        t_i)\land\bigwedge_{(u, v)\in T_i}(u\to v) } {}\vspace{-3mm}
+        t_i)\land\bigwedge_{(u, w)\in T_i}(u\to w) } {}\vspace{-3mm}
 \end{mathpar}
 Here, for each arrow declared in the interface of the function, we
 first typecheck the body of the function as usual (to check that the