From 10c0912f131cd3e95b83229feec9905965149af6 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Fri, 26 Jan 2024 18:53:33 +0100 Subject: Missing bit in rule. --- transp-inf110-03-quantif.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex index 02917f0..770627e 100644 --- a/transp-inf110-03-quantif.tex +++ b/transp-inf110-03-quantif.tex @@ -445,7 +445,7 @@ donc), on notera $(\texttt{match~}z\texttt{~with~}\langle v,h\rangle {\footnotesize (\textbf{N.B.} $v$ peut apparaître dans $s$ mais pas dans $\Gamma$ ni $Q$.)} \[ -\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q} +\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash s \;:\; Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q} \] \medskip @@ -494,7 +494,7 @@ $\forall$ \\\hline $\exists$ &\scalebox{0.80}{$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash z \;:\; Q[v\backslash t]}{\Gamma\vdash \langle t,z\rangle \;:\; \exists (v:I).\, Q}$} -&\scalebox{0.80}{$\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q}$} +&\scalebox{0.80}{$\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash s \;:\; Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q}$} \\ \end{tabular} -- cgit v1.2.3