algorithmic type system in progress

new_system3.tex

@@ -81,7 +81,7 @@ TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
     { \Gamma \vdash e: t' }
     { }
     \qquad
-    \Infer[Efq]
+    \Infer[EFQ]
     { \exists x\in\dom{\Gamma}.\ \Gamma(x)=\Empty }
     { \Gamma \vdash e: t }
     { }
@@ -112,6 +112,16 @@ TODO: Inter rule needed?
 \subsection{Algorithmic type system}
 
 \begin{mathpar}
+\Infer[EFQ]
+{\exists x\in\dom\Gamma.\ \Gamma(x)=\Empty}
+{\Gamma \vdash_e e' : \Empty}
+{ }
+\qquad
+\Infer[Backtrack]
+{\Gamma \vdash_e e': \bt\{t_i,\Gamma_i\}_{i\in I}}
+{\Gamma \vdash_e e : \{t_i,\Gamma_i\}_{i\in I}}
+{ }
+\\
   \Infer[Const]
   { }
   {\Gamma\vdash_e c: \{(\basic{c},\Gamma)\}}
@@ -122,11 +132,6 @@ TODO: Inter rule needed?
 { \Gamma \vdash_e x: \{(\Gamma(x),\Gamma)\} }
 { x\in\dom\Gamma }
 \\
-\Infer[Backtrack]
-{\Gamma \vdash_e e': \bt\{t_i,\Gamma_i\}_{i\in I}}
-{\Gamma \vdash_e e : \{t_i,\Gamma_i\}_{i\in I}}
-{ }
-\qquad
 \Infer[Proj]
 {\Gamma(x)\equiv\pair{t_1}{t_2}}
 {\Gamma \vdash_e \pi_i x: \{t_i,\Gamma\}}