From c418eacb75d4192d26fc20245b765d9bc29f220d Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Wed, 22 Nov 2023 12:23:36 +0100
Subject: Clarification on how to read a derivation tree.

---
 transp-inf110-02-typage.tex | 8 ++++++++
 1 file changed, 8 insertions(+)

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.
 
-- 
cgit v1.2.3