summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-11 10:54:45 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-11 10:54:45 +0100
commit2512fbd5f15ea9c27d32044ca3a1ee6c85001530 (patch)
tree0ab7c9682e0c07c853ef71fe1d448d3c31b62cab
parent663e73acd329df0ed327d94845730e77f3c59e09 (diff)
downloadinf110-lfi-2512fbd5f15ea9c27d32044ca3a1ee6c85001530.tar.gz
inf110-lfi-2512fbd5f15ea9c27d32044ca3a1ee6c85001530.tar.bz2
inf110-lfi-2512fbd5f15ea9c27d32044ca3a1ee6c85001530.zip
Make the fix less confusing.
-rw-r--r--transp-inf110-02-typage.tex9
1 files changed, 3 insertions, 6 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 35425f0..07e2999 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -2675,14 +2675,10 @@ droite \alert{ou à gauche} du symbole « $\vdash$ ».
\medskip
\itempoint On garde la règle $\inferrule*[left=Ax]{ }{\Gamma,Q \vdash
- Q}$, ou on peut en séparer une règle d'qffaibilissement ; et on va
-reparler des règles de « contraction » et « coupure » :
+ Q}$ ; on va reparler des règles de « contraction » et « coupure » :
\begin{center}
\begin{tabular}{c|c}
-$\inferrule*[left=Ax]{ }{Q \vdash Q}$
-&$\inferrule*[left=Weak]{\Gamma \vdash Q}{\Gamma,P\vdash Q}$
-\\\hline
$\inferrule*[left=Contr]{\Gamma,P,P \vdash Q}{\Gamma,P\vdash Q}$
&$\inferrule*[left=Cut]{\Gamma \vdash P\\\Gamma,P\vdash Q}{\Gamma\vdash Q}$
\end{tabular}
@@ -2691,7 +2687,8 @@ $\inferrule*[left=Contr]{\Gamma,P,P \vdash Q}{\Gamma,P\vdash Q}$
\end{frame}
%
\begin{frame}
-\frametitle{Calcul des séquents : les règles (intuitionnistes)}
+\label{sequent-calculus-connector-rules}
+\frametitle{Calcul des séquents : règles (intuitionnistes) des connecteurs}
{\footnotesize