Commit 7fbe6d4e authored by Mickael Laurent's avatar Mickael Laurent
Browse files

trying some new rules... (wip)

parent 4c763865
......@@ -356,12 +356,16 @@ TODO: Algorithmic rules
% {\Gamma\bvdash e t \{(t_i, \Gamma_i)\}_{i\in I}\\\forall i\in I.\ \Gamma_i\vdash e:t_i}
% {\Gamma\bvdash e t \{(t_i\land t_i', \Gamma_i)\}_{i\in I}}
% { }
\\
\Infer[EFQ]
{ }
{\Gamma,(x:\Empty)\bvdash e t \{\}}
{ }
\qquad
% \Infer[EFQ]
% { }
% {\Gamma,(x:\Empty)\bvdash e t \{\}}
% { }
\Infer[EFQ]
{\Gamma\bvdash e t \{(t_i,\Gamma_i)\}_{i\in I}\cup\{(\Empty, \Gamma')\}}
{\Gamma\bvdash e t \{(t_i,\Gamma_i)\}_{i\in I}}
{ }
\\
\Infer[Pair]
{\forall i\in I.\ \Gamma\bvdash{e_1}{t_i}\{(t_i^j,\Gamma_{1,i}^j)\}_{j\in J_i} \\ \forall i\in I.\ \Gamma\bvdash{e_2}{s_i}\{(s_i^k,\Gamma_{2,i}^k)\}_{k\in K_i}}
{\Gamma\bvdash {(e_1,e_2)} {\bigcup_{i\in I}(t_i,s_i)} \bigcup_{i\in I}\{(\pair{t_i^j}{s_i^k}, \Gamma_{1,i}^j\land\Gamma_{2,i}^k)\ |\ j\in J_i, k\in K_i\}}
......@@ -381,6 +385,11 @@ TODO: Algorithmic rules
\Gamma,(x:\neg t_e\land\Gamma(t_e)) \bvdash {e_2} {t} \{(s_j,\Gamma_2^j)\}_{j\in J}}
{\Gamma\bvdash {\tcase {x} {t_e} {e_1}{e_2}}{t} \{(t_i,\Gamma_1^i)\}_{i\in I} \cup \{(s_j,\Gamma_2^j)\}_{j\in J}}
{ }
\\
\Infer[Abs]
{\Gamma\vdash \lambda x:s.\ e:t'}
{\Gamma\bvdash {\lambda x:s.\ e}{t} \{(t\land t',\Gamma)\}}
{ }
\end{mathpar}
TODO: Is the Comp rule needed in this new setting where every application is alone in a let,
......
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