diff options
| author | David A. Madore <david+git@madore.org> | 2024-01-26 18:53:33 +0100 |
|---|---|---|
| committer | David A. Madore <david+git@madore.org> | 2024-01-26 18:53:33 +0100 |
| commit | 10c0912f131cd3e95b83229feec9905965149af6 (patch) | |
| tree | 2b178d91ecfe8d5be79d036343498d1e2559fe1a | |
| parent | 9e237688f4dfc6aa1f9dc30035f3d5c23900fff0 (diff) | |
| download | inf110-lfi-10c0912f131cd3e95b83229feec9905965149af6.tar.gz inf110-lfi-10c0912f131cd3e95b83229feec9905965149af6.tar.bz2 inf110-lfi-10c0912f131cd3e95b83229feec9905965149af6.zip | |
| -rw-r--r-- | transp-inf110-03-quantif.tex | 4 |
1 files 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} |