diff options
| author | David A. Madore <david+git@madore.org> | 2023-12-05 22:27:09 +0100 |
|---|---|---|
| committer | David A. Madore <david+git@madore.org> | 2023-12-05 22:27:09 +0100 |
| commit | 8254a8408b821cbdad5a4bef3cef59687b585ef8 (patch) | |
| tree | 179e617d9746c67f610a3477d82931803322aa18 /transp-inf110-02-typage.tex | |
| parent | dac95486fd7dad3fc7b309c503789a492eec4bf4 (diff) | |
| download | inf110-lfi-8254a8408b821cbdad5a4bef3cef59687b585ef8.tar.gz inf110-lfi-8254a8408b821cbdad5a4bef3cef59687b585ef8.tar.bz2 inf110-lfi-8254a8408b821cbdad5a4bef3cef59687b585ef8.zip | |
Thinko.
Diffstat (limited to 'transp-inf110-02-typage.tex')
| -rw-r--r-- | transp-inf110-02-typage.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 3899f54..9337c80 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -1367,7 +1367,7 @@ En français, et un peu informellement : donne $Q_1\land Q_2$ ; pour l'éliminer : si on a $Q_1 \land Q_2$ on en tire $Q_1$ resp. $Q_2$ ; \item pour introduire $\lor$ : on démontre $Q_1$ et $Q_2$, ce qui - donne $Q_1\land Q_2$ ; + donne $Q_1\lor Q_2$ ; \item pour éliminer $\lor$ : si on a $P_1 \lor P_2$, on démontre $Q$ successivement sous les hypothèses $P_1$ et $P_2$, ce qui donne $Q$ (hypothèses déchargées) ; |