summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-28 18:20:42 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-28 18:20:42 +0100
commit98b27a58f8c5781029dfa88f2d04c2287620a225 (patch)
treec696f169a78d3c9548a7bf964ad36cc6dd033339
parent3c06b7f7286175e089f4724d6c003b770f89bd7d (diff)
downloadinf110-lfi-98b27a58f8c5781029dfa88f2d04c2287620a225.tar.gz
inf110-lfi-98b27a58f8c5781029dfa88f2d04c2287620a225.tar.bz2
inf110-lfi-98b27a58f8c5781029dfa88f2d04c2287620a225.zip
Fix a number of typos / thinkos / notational blunders in an exercise.
-rw-r--r--exercices-inf110.tex8
1 files changed, 4 insertions, 4 deletions
diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index 43ca6c6..6b1f15b 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -1945,8 +1945,8 @@ En Coq, cette preuve s'écrit :
{\tt
Parameter A B C : Prop.\\
Theorem thm : A\textbackslash /B -> ((A->B)->B) /\textbackslash\ ((B->A)->A).\\
-Proof. intro H. destruct H. split. intro H0. apply H0. exact H.
-intro H0. exact H. split. intro H0. exact H. intro H0. apply H0.
+Proof. intro H. destruct H. split. intro H1. apply H1. exact H.
+intro H2. exact H. split. intro H1. exact H. intro H2. apply H2.
exact H. Qed.
\par}
@@ -1960,13 +1960,13 @@ preuve en question :
\lambda(h_2:B\Rightarrow A).\,h_0\rangle,\\
&\iota_2 h_0
\mapsto \langle \lambda(h_1:A\Rightarrow B).\,h_0,\;
-\lambda(h_2:B\Rightarrow A).\,h_1 h_0\rangle)
+\lambda(h_2:B\Rightarrow A).\,h_2 h_0\rangle)
\end{aligned}
\]
(ou en syntaxe Coq : \texttt{(fun H : A \textbackslash/ B =>
match H with
or\_introl H0 => conj (fun H1 : A -> B => H1 H0) (fun H2 : B -> A => H0)
- | or\_intror H0 => conj (fun H2 : A -> B => H0) (fun H1 : B -> A => H1 H0)
+ | or\_intror H0 => conj (fun H1 : A -> B => H0) (fun H2 : B -> A => H2 H0)
end)})
\end{corrige}