From ba309f3d2c416eb056e3bb6a52da783e9bf8744a Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Thu, 1 Oct 2026 15:39:42 +0200
Subject: Fix a bunch of minor mistakes (mostly typos)

Pointed out by LLMs while converting slides to expanded handout.
---
 transp-inf110-03-quantif.tex | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'transp-inf110-03-quantif.tex')

diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 95f05f2..e6c3ddf 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -432,7 +432,7 @@ de $Q(x)$.
 \frametitle{Notations des $\lambda$-termes pour $\exists$}
 
 \itempoint \textcolor{blue}{\underline{Introduction du $\exists$ :}}
-si $t$ désigne un terme de type type $I$ et $z$ une preuve de
+si $t$ désigne un terme de type $I$ et $z$ une preuve de
 $Q[v\backslash t]$ (pour ce $t$-là, donc), on notera $\langle
 t,z\rangle$ la preuve de $\exists(v:I).\,Q$ obtenue par introduction
 du $\exists$.
@@ -458,7 +458,7 @@ donc), on notera $(\texttt{match~}z\texttt{~with~}\langle v,h\rangle
 \medskip
 
 \itempoint Ceci est conforme à l'idée de BHK : une preuve de
-$\exists(v:I).\, P(v)$ est la donnée d'un $t$ de type $I$ d'une preuve
+$\exists(v:I).\, P(v)$ est la donnée d'un $t$ de type $I$ et d'une preuve
 de $Q(t)$.
 
 \end{frame}
@@ -1394,7 +1394,7 @@ Curry-Howard.
 
 \itempoint Il faut y penser comme le type des \textbf{témoignages
   d'égalité} de $m$ et $n$.  En pratique, ce sera un type ayant
-seul habitant $\{m\}$ lorsque $m=n$ et aucun sinon.
+seul habitant $m$ lorsque $m=n$ et aucun sinon.
 
 \medskip
 
@@ -1754,12 +1754,12 @@ intuitioniste, pas limitée au premier ordre) $T$ telle que :
 \item $T$ permet de formaliser « $\varphi_e(i){\downarrow}$ »
   (calculablement en $e$ et $i$),
 \item si $\varphi_e(i){\downarrow}$ alors on peut tirer d'une trace
-  d'exécution une preuve de ce fait dans $T$, et idem pour une boule
+  d'exécution une preuve de ce fait dans $T$, et idem pour une boucle
   infinie explicite,
 \end{itemize}
 on peut construire le programme $g_T$ qui cherche en parallèle dans
 $T$ une preuve de que $g_T$ termine ou ne termine pas, et fait une
-boule infinie explicite dans le premier cas, termine immédiatement
+boucle infinie explicite dans le premier cas, termine immédiatement
 dans le second.
 
 \medskip
@@ -1797,7 +1797,7 @@ Soit $g''$ le programme qui :
 $0$ soit $1$.  Si $g''$ termine et renvoie $0$, alors $T$ le prouve,
 donc $g''$ termine et renvoie $1$, contradiction ; si $g''$ termine et
 renvoie $1$, alors $T$ le prouve, donc (par $\mathsf{Consis}(T)$) il
-ne proue pas que $g''$ termine et renvoie $0$, donc $g''$ termine et
+ne prouve pas que $g''$ termine et renvoie $0$, donc $g''$ termine et
 renvoie $0$, contradiction.
 
 \end{frame}
-- 
cgit v1.2.3