From f6fcfccecaf47838b02c8b3721558643f87a0d52 Mon Sep 17 00:00:00 2001 From: Johnson He Date: Sat, 17 Jul 2021 01:39:03 +0000 Subject: [PATCH] ok-- close to code now --- .../latex/kind-judgements.pdf | Bin 207620 -> 207651 bytes .../latex/kind-judgements.tex | 16 ++++++++-------- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/9-type-aliases-redux/latex/kind-judgements.pdf b/9-type-aliases-redux/latex/kind-judgements.pdf index 79c56e8a4b540df0239e081f5d998160977d1582..62a8a19c29bc0446d1e63fef8ac5abd0f8f24fb0 100644 GIT binary patch delta 11757 zcmaiaQ*b2=&}D2V6WdO1oEzKb#J24l+qP{?Y)>ZE#5N{2_xu0a+Sl!;^Ux1n-Bo=~ zBlIs)$zP;Iawq^V4#s@upx=&|EzVR0`X^hn}zOf4$66fQetuSpImlvvp8R^ z`Jb}Nj<5HbyS|zqRFlmq5E6lNTryhnrXi78JE2)}-^~4osu-P#=ym;Z1i#_tk}8T3 z03E^^LMxspBkf^>BWJk=1C}*5b&tp>l?1MFaU(HBoE)KPb8Vu%0q33)*DAi0(i5y# zQ*^IQB~u$b3Ql?q3Jqj5{Dn9&z%He{icP_~6^ zH%wB3wuEsIT0-HttH0rj@J%V33{Y)|3vF)20Wq4 z4V%Wjjvq=MjF3n4TRv0*D7K9ASSP+2zQGxGEY*qHzp$%y2Cj_E^p|^%yZpJHHgLZR zVyp0vL`Kgd*x6jF_B2^Dq{2QSIVe|B%iQn5L*>`R-)Kr2omhDA5*l z#lFRrawzQ9-_fh+VI9m-il9w8|IcTZ3r#}o6udIsJh$3>$Qq5jQhVE;ejCXz+1ONCKy9lBpNn61YNx~M=$X01zw8%<$$0u2pqnXPNIRFPNc=%nK+N|bN?(+ z6Lw76l(!Uegx4zR0$4Z_nf|;u|I(}6QEgYb2zPy(TqBqYyU>KE;bn7;^ zcm=Us-|x8b#^a?8sO%O?{+CRsz8tf3HLT^{qw~uJV%&6>n0q4yz^WrOVlE-dhW0ZS z7{*J(VE9smJ}ZH6^|<^Hv+m0H2F}yNwLYmo6iZ%kF$_T@Dz6sNAx!X4EMn)15P>}v}!Hy#jy~|`{1P~<$ z!JkIWwS%%%2iESW4j6VI$JpK&Jb|QLjlm7It&*nYdP0}wmBhH6ntA?;L@O-Gs}-Sh7EVGdMI4VActx)-z+p~x#Pe~OtFRXh;jJ-*f89* zj*NcnbbKyLr8Fa|q>7XlZ>QAQFvcD5wZ2kb64qf-QS}{^_&AN(I&f2n1CWk4jX*<# zgnu1Xi-fgKj~1NQ4BU&rLlX)Q*tbc@ct zf{tIkhUKGsz-Om{g$>CU|3saXir(vP?5hW0Y|09n*{p@qP!Y!)LJpuPQUIMkc)s@0 zh5?B!$ecu7B4ZuY`?Fqa8)T?YId@$1qTvw&St6S$x@0F-^UTwVqDm5gV zizUB_(TgFiqK@EZV}MTKm#aMGcDo2WYK1i5R=TNjM5_k@h#s6%Fy~u+*+r>#M9+3r zbqTSx98U&7e8aYj8$bB?*jj%3qG(9SLS4bbz_`kH`dz;y!_F`eXf1$x{}yQo4P42@ z!cdWOCzVi(#M{f4E&K>+6|z`8XHWny!_L7<$srXT@}fCnBV{l}8?6Z)41(5nVr%cb z1CLSdA+5sdop1828oy()kWS!o>{=x{apw9pX#1*~M1R!M7Ng6J_j7E%i13M4M;}1HaeD zV+AEPH04S*-ljlpAjAo5YB`nt;>K=E5H9_Ke#EDsMKE_Tb9HkuH@5#D zO8P&5pC5rm-rT{`&59Jj!^KMazlOjfX>I3bo}vdw0Gig>aM|EO^Iy^0oew|@p4|T{ zNJT`G$75fSw4Oo9u3M;KKMjTx#9*8C(lm2f)UX*VVy3zN^LwJxm)5sB~ z`0aVw>t?_8cIw`Usp-~|y7kaN+9Ga`tnrrj-RVIE?)CFl85ku+7cUgI)8}O`alk}{ zV5}1T4N^hKoI|_OgV8|r!-|&0W5P{$p221dx19(Nqt^X1F(sSMH-XPKN5y^teU-Z7 zA)o<=tT-0Z09hL(lq_?^D>GfonHy?ssTG1+0L3>B>Ko;9ySdy6JN?lTFK2t}H6a;d zh)L8oXH1E+Y94_SiMe970fg|lcve#(F>i@K1koa<4rr?08O72QIdrt5{9(i)<7`2g z8k`DLIRg-_D!bs&-Z2m^&A|~^n;=)MP2Var_;P&uaKE3d&dndX0EINKPTM{{|G6J6 zTA3QST(C>q+D}O7s+M5|l7YjaW19%~>=Dn35p_`hjLy&RDG2DB5|+U96fXFYt&7Xv z1Y+q7_h))u7=MbZQ(<5S?@ytR7rVfB*2b;d!y%l`qQo#o+zZrPlebeQr^*&(tC0m? zEvlpED*4M#Yl1)IU_CtlxvYT#gAp|}a5o}=^fWi_@flP^Q9Cy24V7qtT*VAoRkt#A zNLB{nl5+*gY}t9&g{W87Of)DF(b((*0b-bB)I^MVfv5?#sf_PeIOf*Z*2qN?kc_OK ztU(Q5)?;}uotw~8e;6m7tPu1)AUWOqL-S#3$zV=3e}ooM>wdE zP6z6CrnT!GOcyQaWtr0^Slq{?NC+iC)*Xnxg)HYw@?UJuBjMzuSkAQCo-4FUfq+5G z(g3kQGj6LN8b!^0O;u@RSZ0Nv!nRXBbMf@(1VvJ!zq~hZ{rhl63DGxJBXi@T2uj-9 znx_5{f95NG*ffK|v3A;cT0}8r&wx18D(lGV|7M9EDWFI2QsV_5m$rz<_7~*uIB z&hL64-u`2=@DH#jFTpGh@tRv60cGhU*C(YT6PWljsC8PYx>}L#(D)b=mH_$2%bIE8 z3>+!QLZ@viY3dsvSS{dOw4or3wxu25?Uob8KH;*^#=EB_>Ja6fFZ<8_T0J{y1bwE> zAuKh;**^Got6fFa>5wZD(w2ya+gPTCAC+L@*MoO&xym+VMte3iX3CgUgSaF|K*+6a zkr2OajD{DBa2wwklQ71aR5o;zhzYCb9hRtPS~M;8emVR_Fh1$lWYW}edSPvi z$qpzWv3R=0(*@%@=IZu6zjTPBm(6=UB3`DJOfvrhHH=c5jUHUsZiuU-`9J;+EAG|1{;1^WV4tbA5h>o$yBB6bn7ues=m=Z zO*G^zHksBxStYvQ(uG>p-t6z;GG2nMQ`36=$zAZ z!Bs)UcByIP7rS1O(pzEQY~zuuJ8;|1>6OZ(;!Kk~Xd1C*w>47pC=BeMY3`LRUa`kw zr$F#rv5ZoY`n|6DB&ts<+kPgxrMgz6wkuY2^)P-hY26lY^`eQ^Q$BT0TT!Cb^2!2g zFlG8@8ZZ1=zQ;8w0(xaVYgX-pvcg)Y{)6J2*NEJ^5VCLvT79CzBFiZT=!k354CBr@ zcyJ?NVdDgKnJnhhQ5|53LmYvv$3>`mlBYt z-tO6wV}~i>wAQ>)EJX%N26T6jqrHcBP=|F&Js~*9oLM^)fVKxu)z>}XZ|!mO_bk24=~f&qbO=_i3gjdq8{v{+%S9IHIho5M^W-6 zLtXtKGNMG!I!03-)&2<+F}}I&E_B6nHj`vlB`+uMXHk%e3umyDvw!V~WA`}x&aIvH z@aE*L)u#_?0JUl&ii4uXQzj?}JOV@#I)CR_16*a(9<*cfs6oD8nH-3tFvVAGCHaGsgw%kJ_(1`zF~=!F%o>R zjCCXXs>iP*%H1-}OMQH2{hFzve5Q?hXEy*`%(Xw*ARNIq^5(}9%r)TR`L9U3jfCHS ziwDZLVt#85I#oUGHa)8-=b5%de=)XUL+Jm}_t^# zYf<4#cm$U#!5y*07d21=K;w{@)SPbIzY%3Vfc~<0rL>^ZL2&T=H(t}Fz@ia>(1tyb zi`q6N%T(DiMpced;8JPt}u{#bXyzuF>W#(dm9Z#z*uv2tW-c zU}p#aT8FcssdL%?D1Sa{!N7SrfUO-KA^pnB-iB*S*8ely%5(Pl_ik_^Vi68+aFs*c}>ceMXeOqYmN;lr7<73gk;F5VRw>MeDj+<5lW5*q|s&BRT2i=gnUG9~h@a;jHMzRioq#NizQ5$Egi=ARk}9yMM>!zYvh0 z0`X{VZpcn3-(hGLRS6!!K^i^wO>9a(ut%xVYh}|Wsxu-Gg;UXyYoGzTBJg^Vy0APb&@K`MY(vSaE(z;~yIXEQ z={tZtRMvT0%n1%c-W3xaYzuK!1Q_xM8ov~&_|J7TjE?6xRP@9fq zfz8B1V_YJh>b-dbL0Zm)C$T29JipC?JNJ0=wzuQ2X(lxQUaY%tO`Y_1g^Qo-Tw3ow z=f$}huJ(EqA^LZI2C^hRoGF-+GR-j$pUxibCi*=2Gohokv?&;XUN^2KXTuD=Cbzyp z>E<#8@_e1kW}f-m^kM^^YL|SiEgRAn-DS*mFa70{zWlCpP)c$JW5ZUpAYD9}n2JvB zJWLd~hclQDJO20EGf<{;81BtbRnXLw3-)&mQ>@U#4+KU#xa8eC=V;Y;H(dzwgHS7h zYodT266jPj$En5I7?)C??wVr$fvWFLPa7@yw>Koa{T@?)!Yv%BL~xe0S|FrClj zWScc=4+9^cV-XYNLd2m9J>*cX`nb@xfg!f>>0otc%XyJ_KV1L)We>BgaIW=lkEFn! zGzj&wMQu`fYYgmZiaQ;6xJf!@E!2{A91+YgDSgKWP^x?#^=Dr*Ji8l@pAeTiV61E1Wr zuBS+DU4*x|K4V~(xUK)Gm^U)vXQ7h*XVjEgELsR2o)jfGI*_iMD*-oB-@Dc&KroUF zUU2J->_57pwC0Q3GDvnSUX3n^VrmcgJBJ zW-_>(AKi(d@l`62Q^Pe$!x){Y2nMGJZx)r2sbx}}iEdZgR*`((Dd_Qg(^GM*qRN%Q zQmcPuHAMT(1`@~9V0tla8t_4sOoh{p@sbjuY?~K{pRY|~B#Q(Tx6(vv1-p^{KDC+f z6bN-Iu*mJ{{7lq2vtk> zMVDcKEs6e5-Aje=`V&7&Suym`ia8%MXp&b2E8WbA8Wg!~!i4vz(PbX0MVB-lr`DC0 z%s1`KoEMg=9=Z<3G4SCYi7zqToF{6H-cCA4(JPQ7-hZCV11Xho@W(dTXr6K>~4faPdN{ z6H)qT_`TM=ZLi)#4ysW!;c>kuFTCGLq1?JeEa|jv$~D$iKnYxCqP-+W#wCw}=F)q8 zeXmI;xolt;=~cwd;a(ACQJ+jr3L-u(u>zP1DJa?vYqL&6sys>zj#o`8#~jI;gS{Gp zC>G&B?9>VPel$zj1BjLRC>73FV!#zh9)p8LR}oQaXv>$m{eY9$DP^o9q$jhVCyb=` z3O#l)7&!v-wST!hXgeL&kY}HdPq(5|5Vd)2bD?kg{Q z1R2TQi?18wvB9yFj#veb%bk_5;e(OC}|EWCK-Kyy5?M{Hp*-y8jXd}vJuv9(RKVY_P}pw(ein}4tCaBylGhv zly-G(MH-s|?MDMYANAl!$XY41qApQ=FeJsPq+HOZCvk8@Ww3;fhgP?$54 zI$rOMnI5fBshrlLDDD8LrH-vrJl9SU?zS}lv~&1W-P&zy3^E~b+#$jO(f z0gUDA_ad=DBx5BoVMKI}qr=Df*;P|oG%SY{*d2ANC1jv4uj&LLf-lIp_bY;`tXuHQ z+uwlW+v^_Unz_(FVdY+l#eg$?uOSq|ulAUdUf})zB#5h>i~B-0GGGhU4vN(v+I5qi`sY^Uu1=U7-z zP8WSdj1{xgmCRzj%q?rnBvyO$vin>BwINE%GZ5V*RhmkT|NdU(zA7?+$^zR?xT>R- z*xT3mxU75)qd}Incmya7x?IOIM6EW^V#elG6DQjrxVxic)M6}F!JQW3)?7e3UhXAs z`-{lm6<51o8ZXxifdE5DLu=3`YMns5@qmyusA%J&yoM{lnxWsU6GKt%28;*Baqfph zFBm<6AJA&DRDPiUt^OOSPe@X1Rd+`rqF3Ktuv=3=h}4 z_L_8S=jUvQ8Xr45uEy=Hg5vp0A&E8o>=z&kfI)!u9*@gcU^TBp8eB2-4>{KeB|-%b z8p|Am*_yC3zg&_&-MGL5?A4NuxK6;Rk#Xk*LC_5=scT^DtOx(;| zv_v7yPXk$HyH*Q8kM(JiF|Hy7?cy|pe>yFR!A>V7##b_h=Pxzl;$BQWnc+V&8{_om+_MFB%SqcZ6pdCw{-?#xU+d9{cf`>nc=P&Dq$>7nSaJrl>1Ya&m4T{kx0`!=cP`QRY`>)+xyWw?=^;X4?Fes7N|W-639kTj`-7% zE}TFg84_UVeO^C{G6ag5;R{Tt2ft}JA`4^+Ckv5I*Urh7*inRvK@AW^7|a;{IRwjtvhB$))(a&Z8-`H9QO05+v@gyCnG;M*6goWcKF36$`5G?_&SI8oP-tBFedi+ z+5Ie}M>WD|&Cn%^)QiFxQW@Ql!lJ`k+}N?U=O8u24-lCU>D(B9v6MzH&HYe?6)41B z2-n8-xe8{Cr87e-XH5?WxfZi>)T+7tJIjFqaP+ae3GMS?p&iyT)RsD0!lYBm($`W? zaCC5napm{f7ulD3#EZ+RXe*IB6G=l&v^F(HA4`$f70<*wSl7YEcS%aDJj~AV=h5jQ zxfvrSc=KpMNyv68L&=5ssDuiqkR_==b#Y0ktEe52>+Hb@V$Cyv455M*rAw-~1IgSW zteF{G5uxJXlGj5;WkoRHOz4oeqL#FQ*@~rOY*s3X2&z%Iuuwhf>*zhfI+&W3bT9-5 zD!xo>a9{>0M#&&Q+s=knPZe88qArD%1pp2u{>IY$QnEOTS1&Xy z_crw?ezs+37EiU4CZ|>BR$!W921Pt7Z0scpP`n7H_w|6 z@}G*u8VUE-Oq^`OH!Edgjr+6d%bx5M&-=KQ<&#@0$G1Ar3+-t*MXR5B0nC!WY_ zbiiAb6!C)9Xo3*-Q6ja)O=vZTh_05ken*$A;(tX-POPsv1S)L6v8oXb{3)l1)n6eB z(b|b{&Nf~pueu77RI{|Y=)*QDR!m_*wOqVEuu<`&G|ESgxhs8ZqZQ=z*^18836U2- zYeD9mbeaSW{t=#eoSsTFc3f*e#~$IEY?@Hn>Qag9T57)dGt%j=>E#$zgKgUp{>`Sx z4)#tu<1{@#(WE!j%cN|JQu+OfBF$Jc4J602$l)b&&Tnfk%mZIOuU_7oIEWU!zdBP!E?|b3lx25Qts%g{5 zGM{o0bX~!P%lUY6``Rg?z_Fl;cQ0s-ZBmwVHAUoZx>!+V+tlT-zNa%!Q>awV@SJ8d z&Q=V{)}%g4E`T%r=bRvSal`K=+tg8J@OL34BK0w{io<5SiLmA%yKnxGuS(#G>+OCkl5Hz0R_Ix` zO<^`}lppDtwMO%Uku3FGFIj+Y6#Jv>L$NU0BmLSpt?!37km(^|Ko94e<-0;|mACF; z{OjXg^2_nfXv<4SYSg3bE(*2nT%kEHwU9n_fREnE+{_>u-5vZdnZ?eavB&_?4|ID_ zWa|K7G)2P3JbyS#t_&j`Yp|r;fk>Jn>%mV8OyVGq%}5aO9cJ3*S6OhGU=`HCs1)rz z03BZ5U#LO%SWGF~OEN~bE^BNsQSeNjs;QGTk}4D(#fe-q+?7xWisKMKK_(X@B7+Yu zBEscQl{oqmuZ{Bt;XmF>xl+YaA~O#Pt|xMeYm6;lX#d0IAPH_L2M)g(pN0G1O4Bve zf`t{}M5m2y*T7V3g|#!EF3XgdBW}#gyn7mT(DCaMCo{^Kke7dKLC{-O^p4D2H|L9{ zQ{U0Oa0AHugGV$%@I)>zHG(ro@Q}Hhxg?aK6oa>-EEKcg;g<*Xu(bqz%NdP)l@qkh zH6ZxNY*ft)S+61;$V3NTF}RA=Z0(%%n(|Jos4i_>W)x(!t0GdIQo-hg0D-!c%YH*o z#W4Ti4OC>%)N5w2GUMs3d}<058axB7$@U0nx2OL=z>ciEK{;s&`o6i$19u za7!QI_~Fz$Os%xy+$pmV&?6If35w||kG&9KR6V%v5Fqt|$}c%Y7ltK9 zYlk`?>I|))p8xI{m4Nza;*u4#h%_-to1UO-hJaDutDfd`R` zo8Uo%DyYv72w?b-y;7>_7?kY>0DVSE`|oUlxs=6$2gy(Hj8sX9BYyl4(iX4kZO-hg z+k8+gro3LfaDz{#YU`UJ4M}f-MLgd7 zX0&i#Xm2z^o{}z^5i9i>e<~8-dx-p<)?!cc^tLB2H1C{)V5HcW;T44_(F56fx;SVO z?R4QUW7Bh4Z?Sb3>D`E|#4WpRkKg-*|h#y1IV;z6#w@r>Kc|zQSezXxyf2{LESl6sqOZ0WQIP6-|i3%a$aJEcj z{ti-6{Yg=llz4j7l*^qP!QQPLd&15=UB}_t_aoc4y0}f@(4Y&C<*{~Lv!{%6vS}WH zMK#Q65|KbmZqLKsJVK!a#J7>)e!PO?ZcxT=5*e#5M?>|S#id=#)LrlUKm zF?ul;bys0C6QGAh`e0KBa(0V+zCcSJVq|-?mKIRnW7|n`WNu}AvxnC_u!-zZK|jW4 zjc29Sfsn#`U0>>Jtim8tgnQCa!xp>Plmc$%by0Qdyl(XO^N)$Lg}WMf(Ckmno!fkO zdH(;Ga_8IZk4wPyI|d5!XyZC`O2STV-!?@m$e{mHOh&E{N>=$w zNqNDu=s`RihQ^XT^VgIykY%s|yBtf+a`c~4BL@tAm0+JKlGQ*hy5)b6aT_W>Z_96N`_Hg~2J=1p_`t*E9 z!days7qxh0)^=gTl^?(iVgPk#F<1ZCn68<0#t^Y|macM$JjP6rQ>7zzga&()3#f<E|$Z4ga7sYdRy@7j5ek~*nDT@=iP%|7Q^|g7*A};(v^X1P z3ga#r-<$QlR+QO0I1of|t}aJIMS%arKX6eiX=Be8AWu3u3V2Qa4Y>rqz{8X?w{-|u zaqqgT%PS9!t8{&~`X0VzQU2(~`V1li#)CY(9xb)9Q})^skt82dRy9s^5S* zu@zcTI~X`7>C3fmddvv^-JBeX=O>f^XKOH_1y|KE&*WowtI2Q@*QeS<~v}Nvm01MV%xuv zFeXRd<2QR3rdj}qZ1{2cSB-Fc5Jcu`ZQO)Tm+#Nx+Y~`GFd;)iM_#bxH9gwU$xc~n zM;0_mg&|wj=g0Q6-#EFqiw7M_76xUO;z&zNxZHVY-M3fvz>136zYGq+tH&Td631ir zeR_I!#sVKlJUj4&a*}`mTllnRwaPb-`?m;S|0dP?L}yOS;<|sfmGhCh3TiW6i$t0Y z7eY1cwbb_cJqPiF5c^j53bw>W3LB1)4Ov%5=D+azyzfn}hha5qBCz!Ty}ew-;1bts zf{r7?3Xps>zPA5bQ#klGc{<(QJw#}Af6BzilG67;kL;wMrfD)|<1oaHXimh%*>iFg zmsLc-zIVUZN?z_r?RmN+8GW~%80%EN+cy1_b$hwY*c(J`Nbod##-+egid}r!BOuAW z;Ge0~L$`g`K!0W(FU_8Fd z@zT8QXsIk=dKvrFkknZEH&hM_tG*@Pqy53!e5elKAq6@agfx(N;1U^JG>{zN+(hYId#Aftm8(pgnhOoWGrT>>D^E-uQ&&A}=v z$<8Vc5a$+UlN4iT=im_}<^TV>=>NaJBz6Ed>3?ShS`gJ-r>vL=*4XX+w0o3pJ)nk~ z8lQ6;_n>d&sH*``A7*qS2bbO#WJD8vh+GTF#f7Z{k4*%GrG67E5gQ=MtMakWJe|ZLKA{dB!y36 zjY`y9kSwN@T$jnEl!iT{l#vG3TziPbv*~OlwnS>89-gZ)K-2N+^d>gf9Dy}i)^Q~I z&YeS|Fnni#D^BWs4k#SyVRx`tA%iun=!6Vh3nctSlfRL%#U1ls!Vlt=v56bXJ!u^? zV%}*TGnN&sgU`%Btdq&SW~n1&yl(o7#T)p89)a;h>P~IjnA&#N)VAGDS8dx|wQbwBZMV~@&%gIM_vb2kl3e7;P2Mjl zT0sh4L5e4XVq;<9O*3+XpaEV3>Nn*w70n{t zwI`G1RGdCZ3vNa9L-@M1ODvl@{`DM~Ins1bEH5=%1uRP=(X@L^Wl^7~k*5##2 zc`2fzt|2sHqUV4!y_W1+3olCrri6q-><@Yn;!06fDv!Z#=#p||`dnw_E9qqFOG+~2 zS})jMOCJz*~)ZZ`|g%Pn(nebSv5GZ)b1mhT_5_?<& zhD8k_g~zD+lA^HA````?CzQZ#1I|PV4G!NuyT$eMg0w|C$*uT22))l8h$+37I1JtPnvXk%nv3@krXbN z(*+?QcuFPQ>QJ*k^h-7&{sY&2o<%+}qDGJ4v4nP7qG4ha-@V!binaWu!LO9>g^x^9 zyG=!?f6Six@Anm-HPGuDflF$J3wv<$Vc%PBy9`Pk=q%pdV~NIz55O~7cJD;Nvqu|5 z%Z^pSR8>9)k5whU+_gaj=RHg~&sTNyb+Aj&5}AaO{k~guf#U zI0vqo2)J~p@Btv5RvG+~ccnefeo(yvkBRFa{zxu6Upf?2KwqIqYHCc=*KC@Z^v3Le zpQl%-U{ja}7PNFc?veHB(SSMz^|Cp4uxyT6(t=aVfVmDTMX(nnUTuBSo!S}jsYz=< zZk5l)brWZjCr=t*dtO#?RO?}7suON!lu ztm~ru0p$GW$3D|eG5kV2one4D_od*bFeY*VY(5~>sUj4fS|mK**sHUAh=A`mLDhAq zQJ23n5L9GJG&?vQ7$ADBaKH(@Mx;g_Kj5oGcIP&DL5h61=RSz68Z)(MNC25-^=(;b z5z7@9`62MrtLSwn;Wo!4AZ0_99^OPb2OeR;69SScOuSlm;OPB6m}Y@g6vHF82sZ=f z;urmkf)to{Exhm$OC5O;N&4|VG*?S(bOH)55RxCD!19LSUymgkaEycz?O+hgQ;DVH z`tWdYbX#ErQH4n+s!ah0YAcz)`g=4e^>cbZ&Y=$mhT^CPtvdz;HN7${;p+DgRVoG` z#3he8jz>W|&6oJ=CLDpz*efq}J?T!E%RFpU+PZBF{%Vwx5~lW5p6nD`i^)#9aGja~ zJnrq91STze4wON~Lf~*_GA?4>ZSyo|lQG{`ucUGR?W>Fbtq*Mz+3!cMy?5leHd0Xv z7T*U%<^u6u1+Igs{u!XSYS8$T-Cb7-bbvf3_uR+C9c#BHyY^cE@=mG`@jqF6@H7<^Oxy^om|Pc*;VmfF%w5u2 z=)vv2kb*MT8*73{v@bVcg>S&mUa!H{?z5g?Xb-{HHYq8Pp$EW~>GBQGA$68Pd+(lZ zII|CFz}lqQ{%ah*IvRIR{wpB#uE!;~ki@8R#f=EJmwe&1>XLn+)8uvA8s#7mQ`(X% z*(j!=HqE%R|BA{O)!fxG`aPym*%lrqf9et>XkbvY((2(Q#^BTR8;e@ahoX8d)_l)% zi28TMAlZcrcC9gVAtN5+E|nLfyvXK0MIa%zB|O2EQA^#jA!=ocm1AOM&@IG*4?47~ z>zRc5=ijN_i5T@!Kjh<*CfYOLSj)=BMLDvECAqR$2vprEygY7+5NA2ckNoUTU+hMh z>DfgIwq1FmjHYSBct_S4+%(9e1bBX)NXDT!Omayj*g0OfL!9z5z4e+w7s@_D_$L+Q z^2uOf02{37uQ=%+YH`SZM2M_(j?8}3jI>osIkNq#WO5~GQF~~-=nbC0caz_VC%%11 zL2xR1{5)Kmf~_#o@JQCfIY$*8C(F%=@@dO4R$lG8)KLO5)a`_oh*>Gk>t9wGDXRqU zrT_MKyql*^cKh{0rP7Me+!8f2Z<9XMiutN*qB@n9+1TIjO0CQVBdLl}XZ#&-Os1k& z_C)#O8kcP|hU+j7F`smRhIm!EOhmG*d%K4aR&1Hr*lStC-ou~IcG;AT4+RXxI79)>SW2qpDc`M!7Ea*skusV*JDg>Nw4aVuelT*}n!u zx)=QQ@vk&pK%ZpQZ~MUWVigFz{;BzBrCTM3G`!Ldv#8PyY_fh`!Hp@GHJ`~lmG%asF%6pDv3 zM5=fAg?7?0vL_$|tZj`EzevAwPW#cnLg@gSD|=6T#w{8$8LKTFC+%%6(r*SQXJOGs zH=A`2Q$^kiwB8g27KE%RWm8xgXcCjJxA=w)dwilq5r=^B#~2=t!nI)G`&8BL$y!;E z*b)UuemLiLBc}fV4T!~iUP^Q$@za_U>mUM{2vVb zS=G9m_d`Q4#A*FYd(Lw{WW^t|)I*U`ZbM%~)x%N09sB+)h$$1{PZF8Pu(>!cFUmg& zUFY-HU05d@r@>P&{<)WVG{`|8&%hJC>e%?BTp1LcR#7(+juv^ZbN{s$lzh=SSm2Bh zCrjk_v-kBRC8fHxi6O)cNcrVMX(%e!hlu4$ekWpGV=9fUJ;M8Y0#~F0H#O6ivXqTp zXJ36jF@PyWhZ(N)v*hwz)zXoJ$QREL`9mdSLBFnW06?ytdGO?X_f^C&bC>5(hm6qk z&w|QZN1Hmi*|UpAGROdfuw}_8IeyJ73?;mgq-By1!u`@iZT_bjusimMhCR7YQ#Qgd zy5^^Sa5Kt8RXizYBT7h626)kg31(yg29x8F7Ef6*Iu{ueKy@)|kkrbD<<*({^L_5F ze|-4pLb)?&^Wvp-wOOes#*4CQmc-6VPG}>s1_Xu#Ej-5Z1M(o|&XY(LEmDKh+xN-- z;hYQ-%Xr^kh+ak;h|6Bj+?o2P`fg(MZ%p+(4Lf+R8ego~CBR7=zxo*G=X3@Ih6&=n zzviaAts@!brYK#dEaaMzj)tuy89E0Jlo5C9{@K?98!TjqxRIe3HW7@^nMvnYUp`#r zy)zNGxP)BAq_FoPC%c#QrT>=XpT6U&x!jIE4cbi%-7Zvm;3aik!-R2jQ#f-yU3AR|tkDI4r%-pTwWniJ1usSqtsLr*&+TtKX`s3!BvE_vkS z!Vg`G7?N4fVSyqRzerP=^@-|ktYGf2%wVoZWg>;znK<)Lag-)S>EjnoAHcnQdl4R~ z;O%TS{VK=}*et~x!6c0n3O;T>XI&#^=4P@;BSur!*BP*qzMN0EOvWV|7ijt3cKGhg z9LY=8QlG#}(8vBp%929>VM>|q|kxG@9dP&BM%UZqo)h`HaEyhFElxjDckELzO)53D z6MbZXZr@>+GU4r{3DwRx-~_oZ64RU(5y?D88EM^E=lunMKguQt0y*a9ikBseXzo2x ziidmP>x}Izaer=03WQ`(3CCsFY%>u=Xl@aL+WnVQ;h$yr$g1(#cek{X*Yc9G&U=$G zS>FY^`6iuB&LS9Vi)@q$kcA_5@cfgWwVecjZ(na0CtQarONMrT`bS6{RJ8C%(+`3! zZBYo!rqX-2za}27dK#&cWMl**AIZ5gO4}6*YRP)L9@lEi;zz1c^S~A2?e< zlKsP*Sj{R9w_F}@)JU^hUtFaKGLtIAElx)748{IZgiE3-A;H0vE@!o1^+bl^3=Ggf zGd`4+i5Bofs>eM$MLE;8n7)6w&2fp{rJtSl9s>k@_p4Z*>O3l5I!XN|Ve7W+dS}bR ze4R53a{%~a`A#+F?HmVFJe}X=`ele_=UjSaS@fG82);B+gx`*TSjSh;105&_Z8jKU zodvvkyWd`GHC!wHOwCvAruWGAIts}HJF1eI!GlFNCD(;+c)9lfcsnY5qIUZ7kBpUA zMw=%r%lv_9%G!>B2wO*{T;|wiKfcH&0kw_!(PgPsj@qp!JuCX8R!`Xnv}M>`w}8)Q zf#fQ(#4w6L9o;!Qrdc$hlPBBQzu;*ljMz2la1Ms>UE(gV4zL#&uQGdr=F6Lbc0UfX zSom=6Cg{2bfHOk4DI&ARZPMu5#%x48n3V^R)8KtIJa#Ct*xTZPrpc&>2Pk(;9uF+! zQkfAH{E1NeoVP|42^lA7%EQ_^&|#xnJ8n+5P->^rY+8~CKl0WosbEx-pG!X8FTLvj z?Qh#uO*HZ8?r1u26DL+LLCg~a$>&Yk;Olbo=1rI$%mGu`D_DXpLyA;j5ylo+?MCtO z^LnFRucganmA@B+@{6b;x0Rs}-}m|q^Qu~{fqb>BT+Y&>iK)fZlrl->JLFy)`lO&W z>*gOOnO zj=oMIXSL&^P#+b!JjFDlIr$nxPv6ZPG0& z5m0&12^qX)Yt1?8>s`pYc-dK^TC>5pUD&8kf4m59X3FPLgw}~M+4GljRIkHGkk+j( znuw%1{Rj}wt_evN(Oq$bX2f8qG|8p-$zw3#FMb>V`B&VpF7MHbds>^MkJy1lCWq84c5nuE)(zV|>IoB68N~lp<#@dmO z$d|AW&aY_>6SOSJ!f%!GBds;)KP~<*5a`#(E01(=+kRGUNWWgpvlZUh&&)`e?aG6k zR4)fRRLzmP>L#Ap|4U_bA?=zE&@+`_oG&tY_ESTKTb13lUcH{sB65IyMi_%42dLg3 znUE^9!O)1AiGWUSA|Yn|!15FCAgQu8E~z(kCRcY$S0U_3$$a^}u~R~|(FK~37qhSB zSXx~M91q`L*@=lu7F`WW1|lD=z5NW;L234@y_@khAKcX+_a0T~=*eg|U&*-%T{eGX z6Fb1U){%w@+&f8&3enXbg^8COAE-)?(j1LpNZ`Q*Fix<*!vKKc!%P9j8vQ~9l$7n9 zkD3F!luyWZ7M~ynr!^e%|Pj9X}X#D>^3~YYcJ29QI6)9pAHn4cN%t;_eF>s1YdD+|2vMJ(= zgDg2-mL{I+EFi~b9g0V-T(Uam2=MMLsI!MHH^$4)%nUcT@rx*s#%8pI`+NKsit|cc zu@)25B3btv(4m|LIrDaQfC|Lsmolt$vX;BKKe%wq|5#-FF594{>~vk9bOu$DZS^|o zry5%XQ4DAoP^@cQ`E|DKIx<`(MAaK7B+}64zHyVmk~<}^)ph27LI10+M-_Sf zGY<1vRtf7~;84?~Vu)&y{21P9E9C*O+FG(-1)@Z>`DH#GDL7_`1T5?;$1}=)a@*OJ zFZuQDwfFV-E$|vGvHr7&W>fTX5Goza9MV5j`+TS<*i0rn9bc`aJToey_*-|BeJ{Ix?R`{2BsZaWrBZLt%&;Y4CGKuQP)4GZun73g&U8w=>8906`1J&YWmgR|Vc8TxAU zyaoCOi-ijHx$u-O`zT~xN1hV+GN#pkSeNeCPuhEQjW=knZ6I+~pLwfrHPdEtU&j*2 zB*KgspjfTea+I#sG}jT@7JSy6EstkREX>Oo!1?nRej}g%diNe)PYsTeYxx6F2gCEI@bEvREe%~n zh~b4$2BdY1z$1fOn}Ap`Z*+qk2bIZVkT}UV&7t|cV1x{&P3Q|!`6A0gqh+iM)tj^> zCFwqPVOeonsQp51pLR|zU$+M*`$+u)|2{u17^L!`C6d4w@&7D>1<+^N+-0A43bBzt%JfDK-NdC3 z>)c$u>I)&S@^>aw-6Uy*_)HQ6{%)!wnih-0Hc!DTiQ34U#tkos8cVt-CY-Os#RnIP z%gtZ&H6LY34*~OC+`4q663j{=25F4J$D382{(W4$|7w6cl`eTL8q&9tTHB^@S1O|g zmzLqeJzwiF(@5P_G1W*}jWv}sQ`iVAT8!iMftG?0>^Br_IOJI`XMFFX2Mds4R~VQ_ ztaOVtIXKF0mL9#x+}p>KyWH01TfzRQWl$g(+p)9aUk5J4mkV?qP(XyN=ps4U-^d^v zDwCY=ERl$ixU3EpXcA&OYEG0AaW_KbFat{Q=YO;dTL!(y+kjy<4Pr{0sF5I-3a@p7 zW2Dgox70i97s4x<#%w$UWeychzHVGubIy4{*AyS}9Ve57&cU|lL5T`8dMilE{w40` zk5|4rzksD5$SK9I(S&(V-6PHEI0o(8@D6FmmgKe`h#cVjGOD6AEU)pY1*4!HQ1DiC za-s)SaU{MMZT15JF7v#FYY?KOe9>zi0SGsjZ-F8bwvUE$ z++A(c7Hz3qsIAVO(>_d1PHkBomfCV+gNU&eqP%0s%zjs3y(&oFDbT<;l9CGC0)l3X zRbbjW3cv{wv^mb(SG8co_x)^!PjcWaU9KPgyJj8+LtmnLD&|d?_3J6?GD-qPF}o&f zpfq?f0aIk)?)2S5;xX>j;Bgzi(@WsDpZ9Z1Jql1vsAC06vY*|WwpZb`iO^#_G5H#KlfnivsQZ?5j-PYr?UcIv`ZVDbs&xG z-(P&1OFvha2?QJzkOf-kb&4ejEjz&xsKS46GW*C_y%23)!KCzySUan3rVFsAnKS^R z*v)K(Vqs!9k4m5yEFl9AX*`&#KJZ>DcIHW$62_FwBcM2K#`?JAD5OiG?=~3{Y{iOt zCRk$X{|o4otZ&;VOx2#?5MMqg0AD*_z1DhZv;;cbWs(n^H`=GzBH}VX<8fgPtkwaz zy@@Y{y@M z{`5ti*X3F|1yI&_JJ*VnU4m!Qam-p<<`R{$A0!kDsm4d*8F-sUX2lXlKvTXO&h$eB zV)6>uf4CgweM(J45TX^&P56jPA5^LXguMjQ$*Ys3`xTMrY=I}S@k_yYtK!|-%e6QO z$7AKFs-ZHHr}9Jq>0~-kU2YGI*Z>1JM#p2mS+)}d6!WCVz1X$f@z?vppKjxt)2Taj zZ2v}PxsnauM~YwKYWR~kz#lXM^-s0dg*wZp+ev$o_#TQYyIS;}?;q>ygzI|!V?TG` z?0!gGxdx}UBvjATs+e7Y2OpolY;Xi+foiA^x2(y18 zQ?;TEu;j4TkE6XS-_mO+T-zHbtvhUYobJ!*h4oTI-Q0pJI+Tyi1C<=TAJ2I0C%v;s zvo>j#M%cNIbZdEJ7%Xfr1Ju}B{?J^=PG{87j>2}wj3CY{M;;~{?>eA#&qTKl7|NQh z80)UOUh;@hFqD|8MqJ=F3eLpeiJI7uLzD8GiCIz0uS;H_bXYi{l?dj0!)mL?N_T`g z*{b(+65)apgxNBTfIkt&6&sLaE||zIDLiP4{E*DRYT(*BAR=@r(wB5?G^CT9nNM3C z2DDoIsOgm$uyiYn$D$$md5ZF%`t<=sK>@F;07i8>436TY}MX7PW4)v zE$~)Fg`931*!r8Mv!z@khp_Lk=0@+8mOz2LW9-APm0qgUiLU+npJt%lz$&%|zqPwb zqwa@4eh?ucJx`5#3|aTKelx}P!N z^?E{JZpLjT&%cHpiz=;1LStHQMjXSrRNe{mV`|{3rB}AHI+nL$3&oJ~ zzQKBhbw7fTiNcVHz*~`tAddc#v9PgnvH@rjm=zpM#f@CeNNB|Q*!~N$aI&quJ4`y8wjbhG`Z_6PM{Da6T zOFdxyLFPek!C=?RT*gW!LrBg&s)YuvI`!ygW`@0Sc8aOGOcb*ryimDgjtx^5OL9Sj zAzLj3A*8irt|EM7@lh0k5b+wZT;NZqs5LXJB-Vnr5+UNbE<-deD2^kZF&W5Fz*3{E zxX?VxElAB88_Jc?V}&O7@YAg!v8Nhe8{^7KSx!wAfSDfP^kj!<2iffML?~uNim{3& z;>`G|Hi2VVVacYrfF_F~jZQ$RcR7HUS;`&~m0M%C&x(2)nV-z4OA}Zu*@lPZ6?I|F%FMz0G@ma}ak7}T?!`%c zdqPlKIeR$2^Yr^(We$kkM&5o_3htJt@+(}pvG*fHifF-dIPMqralG&R9=wKCU`x$_ z)dii-BscQdk4(CD#YJqG%FECa=B!v2cfBxLR~OQpZ2(MSc#y?lp+I>LW290{Y-?euJdRK?QRr?cz#NEs(r4y>+F?O8eicui zh!-fJz&LDKm|1eOH|e&T((dxRx^5Rki*dyf`P;3{T>E6N%5fVzyP31{xcBGJ(|#Ts z8dDxSm~gP9YRIia<#y&1L?5#TyLu!W?G7M)YJ1W4jV`YMUJY*`F9qHXW~Un@53~_E zQDCypBi|!SZ71-LyWK6Ie6x|{c9Me_xft%B_S=6)&n7Ux^G*A^`E}UCHCy@GEfmT? z(kooq$TL9ENw(y;o5OZ&?WR@Sg6#AQrMI)--RBZaQOTEp(683A2uT2)$qx0jXqD?? zPJ5BP?Hh+1qvomtzb^e7)YG`@agXY?wxs&vMAL*HSv0VDRFJ89@KHD-{v_2~M^1@I zb%nfSp^R|Uxhj>vg2{c0w&H0(CveNOwJNQ^0eiqslpC=1ZgQz%CCQwW#<^aAbTE}(9eED)0%6pI<&VHuaExMSnq7Dj9Rbc&+gDd7sGgXqUga*>~{wOQV zIeynKc96(bMEopLAi7&4j+S3p8vdUAK7TMc75SDSt|CynEL*El7rO7)?3UrW&KJ?3 z3Gh(gn;7e&Aisd95}Q(lGOw?(nn9lr)kd5u-~m4HG~kW&6$l&41fX*O@KGyV1Mz0r zvhLtE2!?*4zDCH}f2;PZ=BWqXACM=%riVk7^yIBFJ{C|b2oy;augD)7O6R$jB(CY= z4q*(0|GgSIKkA)v`aqkDAB_%XfQF&8f`Woxe@YR?KIAvnJ41XTd`Z+T?TMz6KeO|&)D^1uO8us57PiL-Ic^h1 z7jpiYmih_7&KgS|Hmbcrtt2Zg1hTbR{HAEVtVVJDO=>d>cG{Hec#xF4GGoe9Ep5j2Nr6=(d@Us?S(jbqiBKDGxujZ3Nx8>?n0UJgd_(i zPCF-rbOFwxHi?i*lPAS;y8c?eO{1IpO4LGH@P;CSqT6C^svO}5<#_kGbgX3~X5UXS(P}kS5NHm7 zl;#3iu*KU}f(Z)V%B{IUEIU1+=GY16!zE}-_5;f!-u{L5D?;votS1mK2?X5zuVj1; zVB(X+F&%XmgaV2wFcQ<_q`<}*@+P?KVK#lj_RJVynPExSzWS&laS*7?Xervs*7Z6u zTRZ~*(dCp2v1RMTWA;}2#{A)ic08{vx!gkNW#|4Rp*jyMA!7LLLKLvU#y>bs7zV+ zT}hKZUfZ%lOmlmdC4BwoVH6O`p;~DtP>FW*0Xg%DKd5$$Z2%!CDCjX3vICj-RE}#R zQ;)ea)Ba=Gd%^5p;e(M-b`pwubHi zMHvQJQY3a7znjOjv}TY$7$nZ5_6yCq@P6>J$kN$>I504}1yUbFA05qcN*6P-PBb%l zcM+xqHB>gKoSC|!jzeM!iXA&!ItEzAe^vtQCAai4R-8j) zZG>k9Q>zymN8s#byelo5-^Y^g3W26xJRXyOUnrXC$gp51sm`w$CMg9t6}%*Dtc3jRlY81*Fw;6zv$^Xt&_ln6 zE9nWT_#Jr2jn6Jk?02%+`qtv#N@^s!ZL@7OxnmOqu4~AFhic42`B}%U6`Y9k_2^Ki zA6B&H&nw19?~zBURYi*e0#rbDH&M)tJu&E#noZLZ4_8%84Bsw3yyqnW23ZwGUO$lc zhzndjKTe*Wi3*IuKxd$TVh>_5^#TVEZ&p9Z3}w;FOQ^f+Co9L{!)?*! zCAtV(XS(R&yn@%_0;hf9<^1K~=RWJ@g}sIbSLOj~6Oq*7TrKTos?Fgs)kd};(1*)+ zcq4cdxm3OyzI6#Nv z+vC;;pVzq5KU@a`jY++JJbw`1+lY35Ob153sayq_3;qR{2I-k1LHb?+RxT zdC%FmCk_=^9_rO{U18b26fdWZOllwzsO;^8?T^DVmk~A0$u-Q~IH_NiMmA+H7!QyE zesjqY+tYU838DZud^}_kh>2fR!hvd>A)d<8XREkrS@_L4^H=B*0?aRyY2rlrDDfj! z>%livaqTsWDGt{hl(ynIol@__vB1!S+u}1+qN!OCBq3)x7$dWI~8s~bh@wr}sJ z22@uQ(-H@j29oStU!acMt*J?CRlP(C$K!vk^Pmns>YWd++(Xpvk)hnAbKvUztEDri zUb5Em>b$W)x9mr18(L$P`SPi=6MJVSGh9cLcV;EU*8pr%zcN zgc`>`dh5V-*cZ4xz%t^^v#qaAbJKeCtA0-RF~z~ZKg7@I2~r=lokQ=u#KePITc67j z1od09gGoU}FI6*yyedPxqCnX}hi+mq!tR*MQz5^!-j=?#aPYX@oExD{Y8J(}7y6p@ zW%y6+_Y^-4eT@BMpH$}Lw`dXHYQxstgF6(I3^~N880q_~!SyJ?D=nWC?DKI_Jx-V&3hXQm2@)*@NtUme$bQ)jrP3oZGq5@$*lwTRa?S^kQcfi-*nn5fOddy?MU4#j%Rs5Annh zci#86&m2ZiVAZ!6U^$_>$XC4j@@2&_kN%Kl#A&>T(_4ioC&DB^AAHmr#BtdDW--u> zHQ)95RM-zsc0n|{FB*_frG}(p(z&CwUs&@g@*3_9)aFOE2M@~AdYGjTJzVz~VQEGBTj#5IB1H+5mvGl0vCv?B{p_rL%DA zIE)TSlxd!AqFn#RP}Y368=KOKG-G+dS}h;&Ii4^4v3OFjLGB^~2jlt7 zFcni8@?PY?gU^yeVMxgqgJc>M0u>>qi$P|zAiE*We@=qFAX5m6a!n#yK$PitvnM{H zC|gEtN2|s?Dk;PYONIbI#=oR%LWCzbB?|x5w?X5n@!Ljo{9DC|w52&41IBDst+My1 zYJ>Febq=2|%!#;}%Fr1VK%1_Xw?Z+cAxn?!qPLP6==HXo8CsrgV`kX1+tg6^0bPyf h3`MVwsr}!!g0zulgG+m(gCv3HWI>>$lu(jH_&;nlgPQ;V diff --git a/9-type-aliases-redux/latex/kind-judgements.tex b/9-type-aliases-redux/latex/kind-judgements.tex index 6b13958..1c11238 100644 --- a/9-type-aliases-redux/latex/kind-judgements.tex +++ b/9-type-aliases-redux/latex/kind-judgements.tex @@ -104,9 +104,9 @@ } \and \inferrule[KCSubsumption]{ - \kindAna{\Delta;\hPhi}{\dtau}{\Ty} + \kindAna{\Delta;\hPhi}{\dtau}{\hkappa} } { - \kconsubkind{\Delta;\hPhi}{\SKind[\Ty]{\dtau}}{\Ty} + \kconsubkind{\Delta;\hPhi}{\SKind{\dtau}}{\hkappa} } \end{mathpar} \end{minipage} @@ -173,7 +173,7 @@ } \and \inferrule[KESingReduc]{ - \kindAna{\Delta;\hPhi}{\dtau}{\SKind{\dtau'}} + \kcequiv{\Delta;\hPhi}{\dtau'}{\dtau} }{ \kequiv{\Delta;\hPhi}{\SKind[\SKind{\dtau'}]{\dtau}}{\SKind{\dtau'}} } @@ -260,7 +260,7 @@ \begin{minipage}{\linewidth} \judgbox {\kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_2}} - {$\dtau_1$ is equivalent to $\dtau_2$} \;\\ + {$\dtau_1$ is equivalent to $\dtau_2$ at kind $\Ty$} \;\\ \begin{mathpar} \inferrule[KCESymm]{ \kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_2} @@ -276,7 +276,7 @@ } \and \inferrule[KCESingEquiv]{ - \kindAna{\Delta;\hPhi}{\dtau_1}{\SKind{\dtau_2}} + \kindAna{\Delta;\hPhi}{\dtau_1}{\SKind[\Ty]{\dtau_2}} } { \kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_2} } @@ -327,20 +327,20 @@ {$\htau$ synthesizes kind $\hkappa$ and elaborates to $\dtau$} \begin{mathpar} \inferrule[TElabSConst]{ }{ - \elabSyn{\hPhi}{c}{\SKind{c}}{c}{\EmptyDelta} + \elabSyn{\hPhi}{c}{\SKind[\Ty]{c}}{c}{\EmptyDelta} } \and \inferrule[TElabSBinOp]{ \elabAna{\hPhi}{\htau_1}{\Ty}{\dtau_1}{\Delta_1} \\ \elabAna{\hPhi}{\htau_2}{\Ty}{\dtau_2}{\Delta_2} }{ - \elabSyn{\hPhi}{\htau_1 \oplus \htau_2}{\SKind{\dtau_1 \oplus \dtau_2}}{\dtau_1 \oplus \dtau_2}{\Delta_1 \cup \Delta_2} + \elabSyn{\hPhi}{\htau_1 \oplus \htau_2}{\SKind[\Ty]{\dtau_1 \oplus \dtau_2}}{\dtau_1 \oplus \dtau_2}{\Delta_1 \cup \Delta_2} } \and \inferrule[TElabSList]{ \elabAna{\hPhi}{\htau}{\Ty}{\dtau}{\Delta} } { - \elabSyn{\hPhi}{\hlist{\htau}}{\SKind{\hlist{\dtau}}}{\hlist{\dtau}}{\Delta} + \elabSyn{\hPhi}{\hlist{\htau}}{\SKind[\Ty]{\hlist{\dtau}}}{\hlist{\dtau}}{\Delta} } \and \inferrule[TElabSVar]{