Additional remark.

1 files 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}