diff options
| author | David A. Madore <david+git@madore.org> | 2023-12-11 10:54:45 +0100 |
|---|---|---|
| committer | David A. Madore <david+git@madore.org> | 2023-12-11 10:54:45 +0100 |
| commit | 2512fbd5f15ea9c27d32044ca3a1ee6c85001530 (patch) | |
| tree | 0ab7c9682e0c07c853ef71fe1d448d3c31b62cab | |
| parent | 663e73acd329df0ed327d94845730e77f3c59e09 (diff) | |
| download | inf110-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.tex | 9 |
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 |