diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index d05ca00..9d31d0b 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -45,6 +45,7 @@ \usenavigationsymbolstemplate{\vbox{\hbox{\footnotesize\hyperlinkslideprev{$\leftarrow$}\insertframenumber/\inserttotalframenumber\hyperlinkslidenext{$\rightarrow$}}}} } \setbeamercolor{myhighlight}{fg=black,bg=white!90!green} +\colorlet{mydarkgreen}{green!50!black} \begin{document} \mode<article>{\maketitle} % @@ -1341,7 +1342,7 @@ hypothèses $P_1,\ldots,P_r$, on a $Q$ ». Axiomes : si $Q \in \{P_1,\ldots,P_r\}$ alors $P_1,\ldots,P_r \vdash Q$. -\bigskip +\medskip Introduction et élimination des connecteurs (style « déduction naturelle ») : @@ -1350,7 +1351,7 @@ Introduction et élimination des connecteurs (style « déduction naturelle » \begin{tabular}{c|c|c} &Intro&Élim\\\hline $\Rightarrow$ -&$\inferrule{\Gamma,P\vdash Q}{\Gamma\vdash P\Rightarrow Q}$ +&$\inferrule{\Gamma,{\color{mydarkgreen}P}\vdash Q}{\Gamma\vdash P\Rightarrow Q}$ &$\inferrule{\Gamma\vdash P\Rightarrow Q\\\Gamma\vdash P}{\Gamma\vdash Q}$ \\\hline $\land$ @@ -1361,7 +1362,7 @@ $\land$ $\lor$ &$\inferrule{\Gamma\vdash Q_1}{\Gamma\vdash Q_1\lor Q_2}$ \quad$\inferrule{\Gamma\vdash Q_2}{\Gamma\vdash Q_1\lor Q_2}$ -&$\inferrule{\Gamma\vdash P_1\lor P_2\\\Gamma,P_1\vdash Q\\\Gamma,P_2\vdash Q}{\Gamma\vdash Q}$ +&$\inferrule{\Gamma\vdash P_1\lor P_2\\\Gamma,{\color{mydarkgreen}P_1}\vdash Q\\\Gamma,{\color{mydarkgreen}P_2}\vdash Q}{\Gamma\vdash Q}$ \\\hline $\top$ &$\inferrule{\strut}{\Gamma\vdash \top}$ @@ -1373,6 +1374,9 @@ $\bot$ \\ \end{tabular} +{\footnotesize Les hypothèses en \textcolor{mydarkgreen}{vert} sont + « déchargées ».\par} + \end{frame} % \end{document} |