From 5fd56f4040d6cee45ca87600fa73f5efbce17b2b Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Wed, 13 Dec 2023 13:54:45 +0100
Subject: Additional remark.

---
 transp-inf110-02-typage.tex | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 60705f6..3ded562 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -3552,18 +3552,30 @@ $\mathop{\sim}A := (A\Rightarrow Z)$, puis (inductivement) :
 \quad\itempoint $\bot^{\cps} = \mathop{\sim}\mathop{\sim}\bot$.
 \end{itemize}
 
-\medskip
+\smallskip
 
 \itempoint Il faut comprendre $\mathop{\sim}A$ comme « une
 continuation qui attend un type $A$ » et $\mathop{\sim}\mathop{\sim}A$
 comme « une valeur $A$ passée par continuation ».
 
-\medskip
+\smallskip
 
 \itempoint Noter que $x:A \;\vdash\; \lambda(k:\mathop{\sim}A).kx :
 \mathop{\sim}\mathop{\sim}A$ (transformation d'une valeur « directe »
 en valeur passée par continuation).
 
+\smallskip
+
+{\footnotesize
+
+\itempoint On vérifie : $\mathop{\sim} A \Leftrightarrow
+\mathop{\sim}\mathop{\sim}\mathop{\sim} A$, donc $P^{\cps}
+\Leftrightarrow \mathop{\sim}\mathop{\sim} P^{\cps}$ ; remarquer
+aussi : $\bot^{\cps} \Leftrightarrow Z$ et $(\neg P)^{\cps}
+\Leftrightarrow \mathop{\sim} P^{\cps}$.
+
+\par}
+
 \end{frame}
 %
 \begin{frame}
-- 
cgit v1.2.3