Commit 87797484 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

typo

parent 41e7ade8
......@@ -229,10 +229,10 @@ If $\Gamma\vdash e:t$ then $\exists e',t'$ such that $\eras{e'}=e$,
$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}$
$e\reduces e'$ if and only if $\eras e \reduces \eras{e'}$
(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}$)
$\eras e \reduces \eras{e'}\Longrightarrow e\reduces^{0|1} e'$ and
$e\reduces e'\Longrightarrow \eras e \reduces^+ \eras{e'}$)
\subsection{Normalization}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment