Commit 1c1bf33b authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

rewording

parent 3c6c2c26
......@@ -102,8 +102,11 @@ The idea is to translate terms above in to explicitly annotated
notrmal form and prove that a term above is well typed if and only if
its translation is well typed for a suitable annotation.
In particular the typing rule for cases will be obtained by combining
the union rule with the case rule and using two subsumption rules. Intuitively
In particular the typing rule for cases of CDuce will be obtained by combining
the union rule with the case rule and using two subsumption
rules. Intuitively we have that Cduce's $\tcase {x\,{:}{=}\,e} t {e_1}{e_2}$ is
just syntactic sugar for $\letexp x {e}{\tcase {x} t {e_1}{e_2}}$ and
we have that:
\begin{mathpar}
\inferrule*{
\inferrule*{
......@@ -120,8 +123,9 @@ the union rule with the case rule and using two subsumption rules. Intuitively
}
{\Gamma\vdash \letexp x {e}{\tcase {x} t {e_1}{e_2}:t'}}
\end{mathpar}
Note: $t_\circ =(t\wedge t_\circ)\vee(\neg t\wedge t_\circ$)
[Note: $t_\circ =(t\wedge t_\circ)\vee(\neg t\wedge t_\circ$)]
So we find exactly the typing rule for Cduce's typecase.
\subsubsection{Normal form terms with explicit annotations}
......
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