Commit 5b431ab8 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

new system again

parent 06e28f12
......@@ -205,10 +205,12 @@ plus context rules to implement an leftmost outermost weak reduction semantics.
{ x\in\dom\Gamma }
\\
\Infer[$\to$I]
{i=1..n\\\Gamma,x:t_i\vdash e:s_i}
{\Gamma\vdash\lambda x{:}\{t_1,...,t_n\}.e: \textstyle\bigwedge_{i=1..n}\arrow{t_i}{s_i}}
{ }
\qquad \Infer[$\to$E]
{\forall j\in J \\\Gamma,x:t_j\vdash e:s_j}
{\Gamma\vdash\lambda
x{:}\{\ann{\Gamma_i}{t_i}\}_{i \in I}.e:
\textstyle\bigwedge_{j\in J}\arrow{t_j}{s_j}}
{ J=\{i\in I\alt \Gamma\leq\Gamma_i\}}
\\\Infer[$\to$E]
{
\Gamma \vdash e_1: \arrow {t_1}\quad
\Gamma \vdash e_2: t_2
......@@ -252,12 +254,13 @@ plus context rules to implement an leftmost outermost weak reduction semantics.
%% {\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}s_i\\i=1..n \\ \Gamma, x:s_i\vdash e:t_i}
\Infer[Let]
{\Gamma\vdash e_1:\textstyle\bigvee_{j\in J}t_j\\j\in J \\ \Gamma, x:t_j\vdash e_2:s_j}
{
\Gamma\vdash\letexp {x{:}\{s_1,...,s_n\}} {e'} e :\textstyle \bigvee_{i=1..n}t_i
\Gamma\vdash\letexp {x{:}\{\ann{\Gamma_i}{t_i}\}_{i\in I}} {e_1}
{e_2} :\textstyle \bigvee_{j\in J}s_j
}
{ }
{ J=\{i\in I\alt \Gamma\leq\Gamma_i\}}
\end{mathpar}
\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