From 98b27a58f8c5781029dfa88f2d04c2287620a225 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Thu, 28 Dec 2023 18:20:42 +0100 Subject: Fix a number of typos / thinkos / notational blunders in an exercise. --- exercices-inf110.tex | 8 ++++---- 1 file 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} -- cgit v1.2.3