diff options
| -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. |