diff options
| author | David A. Madore <david+git@madore.org> | 2023-11-22 12:23:36 +0100 |
|---|---|---|
| committer | David A. Madore <david+git@madore.org> | 2023-11-22 12:23:36 +0100 |
| commit | c418eacb75d4192d26fc20245b765d9bc29f220d (patch) | |
| tree | 7836a686a71dcaed621257dfd5302d415f7be4b3 | |
| parent | 0e6c860b06681b7898c43ba522f5b75f3aec56c5 (diff) | |
| download | inf110-lfi-c418eacb75d4192d26fc20245b765d9bc29f220d.tar.gz inf110-lfi-c418eacb75d4192d26fc20245b765d9bc29f220d.tar.bz2 inf110-lfi-c418eacb75d4192d26fc20245b765d9bc29f220d.zip | |
Clarification on how to read a derivation tree.
| -rw-r--r-- | transp-inf110-02-typage.tex | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index c33784d..e150b3e 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -897,6 +897,8 @@ $\lambda(f:\beta\to\alpha\to\gamma). \lambda(x:\alpha). \lambda(y:\beta). fyx$ est un terme de type $(\beta\to\alpha\to\gamma) \to (\alpha\to\beta\to\gamma)$ dans le contexte vide : +\vskip-3ex + {\footnotesize \[ \inferrule*[left=\llap{Abs}]{ @@ -917,6 +919,12 @@ est un terme de type $(\beta\to\alpha\to\gamma) \to \] \par} +Chaque barre horizontale justifie le jugement écrit \alert{en-dessous} +par la règle inscrote \alert{à côté} à partir des hypothèses portées +\alert{au-dessus}. + +\medskip + Ceci est typographiquement abominable et hautement redondant, ce qui explique qu'on écrive rarement de tels arbres complètement. |