From 413e8bdf7c27dab575ea8d63eb86b7a500d1983a Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Tue, 28 Nov 2023 12:45:45 +0100
Subject: Highlight discharged hypotheses in natural deduction presentation.
---
transp-inf110-02-typage.tex | 10 +++++++---
1 file 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}
--
cgit v1.2.3