Commit ccd746b4 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

update Case refinement rule

parent 6ac5773b
......@@ -100,9 +100,9 @@ binders):\svvspace{-1.5mm}
\svvspace{-2.3mm}\\
\Infer[Case]
{\Gamma\vdash e\triangleright\psi_\circ\\
\Gamma \evdash e t \Gamma_1\\ \Gamma_1\vdash e_1\triangleright\psi_1\\
\Gamma \evdash e {\neg t} \Gamma_2 \\ \Gamma_2\vdash e_2\triangleright\psi_2}
{\Gamma\vdash \ifty{e}{t}{e_1}{e_2}\triangleright\psi_\circ\cup\psi_1\cup\psi_2}
\Gamma \evdash e t \Gamma_1\\ \Gamma_1\vdash e\triangleright\psi_1\\ \Gamma_1\vdash e_1\triangleright\psi_1'\\
\Gamma \evdash e {\neg t} \Gamma_2 \\ \Gamma_2\vdash e\triangleright\psi_2\\ \Gamma_2\vdash e_2\triangleright\psi_2'}
{\Gamma\vdash \ifty{e}{t}{e_1}{e_2}\triangleright\psi_\circ\cup\psi_1\cup\psi_1'\cup\psi_2\cup\psi_2'}
{}\svvspace{-1.4mm}
\end{mathpar}
Where $\psi\setminus\{x\}$ is the function defined as $\psi$ but undefined on $x$ and $\psi_1\cup \psi_2$ denotes component-wise union%
......
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