Add T-Elvis rule

constraints.tex

@@ -12,6 +12,17 @@
 Constraint generation step is the same as in \cite{TIforFGJ} except for field access and method invocation.
 Here \fjtype{} generates capture constraints instead of normal subtype constraints.
 
+Subtype constraints are created according to the type rules defined in section \ref{sec:tifj}.
+The \typeExpr{} function creates constraints for a given expression.
+
+$\begin{array}{c}
+\typeExpr(\texttt{t}_1, \ntv{b}) = C_l \quad \quad \typeExpr(\texttt{t}_2, \ntv{c}) = C_l \quad \quad \ntv{b}, \ntv{c} \ \text{fresh}
+\\
+\hline
+\typeExpr(\texttt{t}_1 \texttt{?:} \texttt{t}_2, \tv{a}) = C_l \cup C_r \cup \set{\ntv{b} \lessdot \tv{a}, \ntv{c} \lessdot \tv{a}}
+\end{array}
+$
+
 The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
 Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
 

tRules.tex

@@ -18,6 +18,8 @@ class List<A> {
 }
 \end{verbatim}
 
+%The rules depicted here are type inference rules. It is not possible to derive a distinct typing from a given input program.
+
 %The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}.
 %and is solely used for examples.
 The calculus does not include method overriding for simplicity reasons.