Commit 6066a29c authored by Mickael Laurent's avatar Mickael Laurent
Browse files

trying some new rules... (wip)

parent aca5b30f
......@@ -97,8 +97,9 @@ x\in\dom\Gamma\\
\Infer[LetSplit]
{
\Gamma,(x:t')\vdash e\triangleright_x\dt\\
\forall u\in \dt.\ \Gamma\bvdash{p}{u} (\Gamma_u^i)_{i\in I_u}\\
\forall u\in \dt.\ \forall i\in I_u.\ \Gamma_u^i\vdash_{u}\letexp x p e : t}
\dt' = \dt\cup\{t'\setminus\textstyle\bigcup_{u\in\dt}u\}\\
\forall u\in \dt'.\ \Gamma\bvdash{p}{u} (\Gamma_u^i)_{i\in I_u}\\
\forall u\in \dt'.\ \forall i\in I_u.\ \Gamma_u^i\vdash_{u}\letexp x p e : t}
{
\Gamma\vdash_{t'}\letexp x p e : t
}
......@@ -269,8 +270,6 @@ TODO: Abs rule must be updated (like the let rule)
TODO: Candidates for a variable should be a special "all splits".
Otherwise, $\letexp{x}{\cdots}{x}$ will never be splitted.
TODO: Candidates should always be a partition of the initial type of $x$
\subsection{Forward refinement rules}
\subsection{Backward refinement rules}
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