bla

new_system_beppe.tex

@@ -21,7 +21,8 @@ t_1\vee\neg t_2)$
     \textbf{Values} & v  &::=& c\alt\lambda x.e\alt (v,v)
   \end{array}
 \end{equation}
-
+(no let here: can be added on a surface language later together with
+ explicit type annotation $e:t$ that are checked by bidirectional typing) 
 \subsubsection{Type Tests for values}
 We define $\typof c = \basic{c}$, $\typof {\lambda x.e} = \Empty\to\Any$,
 $\typof{(v_1,v_2)}=\typof{v_1}\times\typof{v_2}$. Finally $v\in t$ iff
@@ -141,8 +142,8 @@ Variant with more compact derivations:
 For annotations we write $\{t_1,\ldots{,} t_n\}$ for
 $\{\ann\varnothing{t_1},\ldots{,}\ann\varnothing{t_n}\}$ and just $t$
 for $\{\ann\varnothing{t}\}$. So for instance we write $\lambda
-x{:}t.e$ for $\lambda x{:}\{\ann\varnothing{t}\}.e$ and
-$\letexp{x{:}\{t_1,\ldots{,} t_n\}}{e}{e}$ instead of $\letexp{x{:}\{\ann\varnothing{t_1},\ldots{,}\ann\varnothing{t_n}\}}{e}{e}$ 
+x{:}t.e$ for $\lambda x{:}\{\ann\varnothing{t}\}.e$ while
+$\letexp{x{:}\{t_1,\ldots{,} t_n\}}{e}{e}$ stands for $\letexp{x{:}\{\ann\varnothing{t_1},\ldots{,}\ann\varnothing{t_n}\}}{e}{e}$ 
 \subsubsection{Algorithmic typing rules} This system correspond to the
 variant with more compact derivations.
 \begin{mathpar}
@@ -229,7 +230,9 @@ $t'\leq t$, and $\Gamma\vdashA e': t'$
 \subsubsection{Preservation of the reductions}
 Write the reduction rule for let and then note that
 $e\reduces e'$ if and only if $\eras e \reduces \eras{e}$
-(details to be checked, should we rather use $v$?)
+(details to be checked, should we rather use $v$? Probably we have
+$\eras e \reduces \eras{e}\Longrightarrow e\reduces^{0|1} e'$ and
+$e\reduces e'\Longrightarrow \eras e \reduces^+ \eras{e}$)
 
 \subsection{Normalization}