Given an expression e, a type T and a dictionary TT
that maps variables to type, the notation
TT |- e : T
roughly means
T = typecheck(TT, e)
and the horizontal bar notation:
P1 P2 P3
----------------
Q
means
Q if P1 and P2 and P3
from: http://wiki.jvmlangsummit.com/pdf/28_Siek_gradual.pdf (slide 6)
