some reflexions...

new_system.tex

@@ -16,6 +16,11 @@
   \end{array}
 \end{equation}
 
+TODO: the then and else expressions of typecases have no associated variable,
+altough the env refinement rules could refine their types...
+Is this an issue? Should we require an atomic in the then and else branchs
+(seems difficult: there would be no equivalent normal form)?
+
 TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
 
 \subsection{Typing rules}
@@ -165,11 +170,10 @@ TODO: Algorithmic rules
   \end{mathpar}
 
   TODO: example: application $x y$ with $x$ an union of arrow. Candidates
-  of a variable with a function type should be all the union of arrows of its type?\\
-  More generally, a variable that can be written only has an union should be splitted
-  along this union. Otherwise, $\letexp{x}{\cdots}{x}$ will never be splitted. Or better:
-  there should be a special split that means "all splits" (it will also be useful when
-  we will add polymorphism).
+  for $x$ should be all the different union of arrows of its type?
+
+  TODO: Candidates for a variable should be a special "all splits".
+  Otherwise, $\letexp{x}{\cdots}{x}$ will never be splitted.
 
   TODO: test type system with $\lambda x:\pair{\Int}{\Int}\lor\pair{\Bool}{\Bool}. (\pi_1 x, \pi_2 x)$