From a9e829ce2e76805f228bca36115a4b225d550f98 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 4 Dec 2023 12:04:26 +0100
Subject: Various minor changes or additions.

---
 transp-inf110-02-typage.tex | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

(limited to 'transp-inf110-02-typage.tex')

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 7e4c691..aff8392 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1828,6 +1828,13 @@ constructivisme russe de A. Markov fils) :
 resp. $\exists x.P(x)$ passe forcément par la preuve de $P$ ou de $Q$,
 resp. par la construction d'un $x$ vérifiant $P(x)$.
 
+\bigskip
+
+\itempoint Les maths « normales » se font en logique classique, mais
+certains bouts (explicit\textsuperscript{t} signalés comme tels) de la
+littérature sont en logique intuitionniste.  On peut y faire de
+l'algèbre, de l'analyse, etc., constructives.
+
 \end{frame}
 %
 \begin{frame}
@@ -2149,7 +2156,7 @@ doute sur la correspondance elle-même.
 \end{frame}
 %
 \begin{frame}
-\frametitle{Correspondance de Curry-Howard : exemple avec conjonction}
+\frametitle{Correspondance de Curry-Howard : exemple avec disjonction}
 
 \itempoint Transformons en programme la démonstration qu'on a donnée
 de $A\lor B \Rightarrow B\lor A$
@@ -2218,6 +2225,19 @@ $\inferrule*[left={Void}]{\Gamma\vdash r:\bot}{\Gamma\vdash
 
 \itempoint Pas de nouvelle règle de réduction à ajouter.
 
+\medskip
+
+{\footnotesize
+
+En OCaml :
+
+{\tt
+type void = | ;;
+let exfalso = fun (r:void) -> match r with \_ -> . ;;
+}
+
+\par}
+
 \end{frame}
 %
 \begin{frame}
-- 
cgit v1.2.3