From 2cf14e0c73464472b0ea04630bcf1e01f3caaa61 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Fri, 8 Dec 2023 19:21:18 +0100
Subject: Fix various mistakes noted during lecture on 2023-12-08.

---
 transp-inf110-02-typage.tex | 21 ++++++++++++---------
 1 file changed, 12 insertions(+), 9 deletions(-)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 9337c80..f3e8b1d 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1042,16 +1042,18 @@ La dérivation du jugement de typage $\Gamma \vdash M : \sigma$ d'un
 évidemment à partir de $M$ (\alert{aucun choix} à faire !) :
 \begin{itemize}
 \item si $M = x$ est une variable, alors un $x:\sigma$ doit être dans
-  le contexte $\Gamma$ (sinon : échouer), et la dérivation finit par la
-  règle « variable » ;
+  le contexte $\Gamma$ (sinon : échouer), et la dérivation consiste en
+  la règle « variable » ;
 \item si $M = PQ$ est une application, construire des dérivations de
   jugements $\Gamma \vdash P : \rho$ et $\Gamma \vdash Q : \sigma$, on
   doit avoir $\rho = (\sigma\to\tau)$ (sinon : échouer), et la
-  dérivation finit par la règle « application » ;
+  dérivation finit par la règle « application » et donne $\Gamma
+  \vdash M : \tau$ ;
 \item si $M = \lambda(v:\sigma).E$ est une abstraction, construire une
   dérivation de jugement $\Gamma' \vdash E : \tau$ dans $\Gamma' :=
   \Gamma \cup \{v:\sigma\}$ {\footnotesize (quitte à renommer $v$)},
-  et la dérivation finit par la règle « abstraction ».
+  et la dérivation finit par la règle « abstraction » et donne $\Gamma
+  \vdash M : \sigma\to\tau$.
 \end{itemize}
 
 \bigskip
@@ -1094,7 +1096,8 @@ correspond à un terme (typable) du $\lambda$CST.
 
 \smallskip
 
-\textcolor{brown}{$\rightarrow$ Algorithme de Hindley-Milner.}
+\textcolor{brown}{$\rightarrow$ Algorithme de Hindley-Milner
+  (\emph{inférence} de type).}
 
 \bigskip
 
@@ -1152,13 +1155,13 @@ chaque règle « variable ».
 \itempoint\textbf{Lemme :} Si $\Gamma, v:\sigma \vdash E : \tau$ et
 $\Gamma \vdash T : \sigma$ alors $\Gamma \vdash E[v\backslash T] :
 \tau$, où $E[v\backslash T]$ désigne le terme obtenu par substitution
-correcte de $v$ par $v$ dans $E$.
+correcte de $v$ par $T$ dans $E$.
 
 \bigskip
 
 \underline{Esquisse de preuve :} reprendre l'arbre de dérivation de
 $\Gamma, v:\sigma \vdash E : \tau$ en supprimant $v:\sigma$ du
-contexte et en substituant $v$ par $E$ partout à droite du ‘$\vdash$’.
+contexte et en substituant $v$ par $T$ partout à droite du ‘$\vdash$’.
 Les règles s'appliquent à l'identique, sauf la règle « variable »
 introduisant $v:\sigma$, qui est remplacée par l'arbre de dérivation
 de $\Gamma \vdash T : \sigma$.\qed
@@ -2150,8 +2153,8 @@ règle \textsc{Intro} immédiatement suivie par sa règle \textsc{Élim}
 
 \medskip
 
-\itempoint Le $\lambda$-calcul simplement typé reste fortement
-normalisant avec ces extensions par types produits et sommes et les
+\itempoint Le $\lambda$-calcul simplement typé \alert{reste fortement
+  normalisant} avec ces extensions par types produits et sommes et les
 réductions ci-dessus {\footnotesize (et types $1$ et $0$ après)}.
 
 \medskip
-- 
cgit v1.2.3