summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--transp-inf110-03-quantif.tex10
1 files changed, 5 insertions, 5 deletions
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 5c69859..e0e44b9 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -344,7 +344,7 @@ $\bot$
\\\hline
$\forall$
&$\inferrule{\Gamma, {\color{mydarkgreen}v:I}\vdash Q}{\Gamma\vdash \forall (v:I).\, Q}$ ($v$ \alert{frais})
-&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash \forall (v:I).\, Q}{\Gamma\vdash Q[v\backslash t]}$
+&$\inferrule{\Gamma\vdash \forall (v:I).\, Q\\{\color{gray}\Gamma\vdash t:I}}{\Gamma\vdash Q[v\backslash t]}$
\\\hline
$\exists$
&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash Q[v\backslash t]}{\Gamma\vdash \exists (v:I).\, Q}$
@@ -401,7 +401,7 @@ type $I$, on notera $ft$ la preuve de $Q[v\backslash t]$ {\footnotesize
{\footnotesize (\textbf{N.B.} on n'explique pas comment le « terme
d'individu » $t$ est formé.)}
\[
-\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash f \;:\; \forall (v:I).\, Q}{\Gamma\vdash ft \;:\; Q[v\backslash t]}
+\inferrule{\Gamma\vdash f \;:\; \forall (v:I).\, Q\\{\color{gray}\Gamma\vdash t:I}}{\Gamma\vdash ft \;:\; Q[v\backslash t]}
\]
\medskip
@@ -481,7 +481,7 @@ $\bot$
\\\hline
$\forall$
&\scalebox{0.80}{$\inferrule{\Gamma, v:I\vdash s:Q}{\Gamma\vdash \lambda(v:I).\,s\;:\;\forall (v:I).\, Q}$}
-&\scalebox{0.80}{$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash f \;:\; \forall (v:I).\, Q}{\Gamma\vdash ft \;:\; Q[v\backslash t]}$}
+&\scalebox{0.80}{$\inferrule{\Gamma\vdash f \;:\; \forall (v:I).\, Q\\{\color{gray}\Gamma\vdash t:I}}{\Gamma\vdash ft \;:\; Q[v\backslash t]}$}
\\\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}$}
@@ -855,7 +855,7 @@ $\bot$
\\\hline
$\forall$
&$\inferrule{\Gamma, {\color{mydarkgreen}x:I}\vdash Q}{\Gamma\vdash \forall x.\, Q}$ ($x$ \alert{frais})
-&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash \forall x.\, Q}{\Gamma\vdash Q[x\backslash t]}$
+&$\inferrule{\Gamma\vdash \forall x.\, Q\\{\color{gray}\Gamma\vdash t:I}}{\Gamma\vdash Q[x\backslash t]}$
\\\hline
$\exists$
&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash Q[x\backslash t]}{\Gamma\vdash \exists x.\, Q}$
@@ -1420,7 +1420,7 @@ différent : $A_0 \rightarrow (\prod_n\,(A_n\rightarrow A_{n+1}))
On peut souvent s'en faire une idée d'après son type, p.ex. :
\begin{itemize}
\item La commutativité de la multiplication $\forall m.\forall
- m.(m\times n = n\times m)$ prend $m$ et $n$ et un renvoie un
+ n.(m\times n = n\times m)$ prend $m$ et $n$ et un renvoie un
témoignage d'égalité de $m\times n$ et $n\times m$ (c'est-à-dire en
fait $m\times n$ calculé de deux manières différentes).
\item La preuve de $\forall n. (n=0 \lor \neg n=0)$ donnée