Commit a2a1d786 by Giuseppe Castagna

### changed algorithmic rules

parent 53eb81a8
 ... ... @@ -178,31 +178,30 @@ So we find exactly the typing rule for Cduce's typecase. \\ \Infer[$\neg_1$] { \Gamma, x: t_0{\wedge} t\vdash e_1: t' \Gamma \vdash e_1: t' \\ \Gamma(x)\leq t } {\Gamma,x:t_0\vdash \tcase {x} t {e_1}{e_2}: t'} {t_0\wedge\neg t = \Empty} {\Gamma\vdash \tcase {x} t {e_1}{e_2}: t'} {x\in\dom{\Gamma}} \quad \Infer[$\neg_2$] { \Gamma, x: t_0{\wedge} \neg t\vdash e_2: t' \Gamma\vdash e_2: t' \\ \Gamma(x)\leq\neg t } {\Gamma,x:t_0\vdash \tcase {x} t {e_1}{e_2}: t'} {t_0\wedge t = \Empty} \and \Infer[$\neg$] { \Gamma, x: t_0{\wedge} t\vdash e_1: t' \\ \Gamma, x: t_0{\wedge} \neg t\vdash e_2: t' } {\Gamma,x:t_0\vdash \tcase {x} t {e_1}{e_2}: t'} {\text{(otherwise)}} {\Gamma\vdash \tcase {x} t {e_1}{e_2}: t'} {x\in\dom{\Gamma}} %% \and %% \Infer[$\neg$] %% { %% \Gamma, x: t_0{\wedge} t\vdash e_1: t' \\ \Gamma, x: t_0{\wedge} %% \neg t\vdash e_2: t' %% } %% {\Gamma,x:t_0\vdash \tcase {x} t {e_1}{e_2}: t'} %% {\text{(otherwise)}} \\ \Infer[$\vee$] {\Gamma\vdash e':\textstyle\bigvee_{i=1..n}t_i\\i=1..n \\ \Gamma, x:t_i\vdash e:t} {\Gamma\vdash e':\textstyle\bigvee_{i=1..n}s_i\\i=1..n \\ \Gamma, x:s_i\vdash e:t_i} { \Gamma\vdash\letexp {x{:}\{t_1,...,t_n\}} {e'} e : t \Gamma\vdash\letexp {x{:}\{s_1,...,s_n\}} {e'} e :\textstyle \bigvee_{i=1..n}t_i } { } \end{mathpar}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!