summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-15 17:33:37 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-15 17:33:37 +0100
commite8dc0e623b6836c0d68a574fba4d58bbc16b17cb (patch)
treee50a92311ef40b1f77ebeffeb4fac30c6358b4d8
parent390271345644bc016f2f456ea770e2a1b59da703 (diff)
downloadinf110-lfi-e8dc0e623b6836c0d68a574fba4d58bbc16b17cb.tar.gz
inf110-lfi-e8dc0e623b6836c0d68a574fba4d58bbc16b17cb.tar.bz2
inf110-lfi-e8dc0e623b6836c0d68a574fba4d58bbc16b17cb.zip
Fix typing errors.
-rw-r--r--transp-inf110-02-typage.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 4add232..188b7eb 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -3174,8 +3174,8 @@ $\inferrule*{
\inferrule*{
\inferrule*{ }{x_2:A_2\vdash x_2:A_2}
\\
-\inferrule*{ }{\_:C \vdash \_ [] : C}
-}{x_2:A_2;\_:A_2\to B \vdash \_ [x_2] : A_2\to B}
+\inferrule*{ }{\_:B \vdash \_ [] : B}
+}{x_2:A_2;\_:A_2\to B \vdash \_ [x_2] : B}
}{x_1:A_1, x_2:A_2;\_:C \vdash \_ [x_1; x_2] : B}
}{y:C, x_1:A_1, x_2:A_2\vdash y [x_1; x_2] : B}$
}