From f220efc5ba787f117b407f2e6912e5ae8f0c3eb7 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 28 Aug 2024 15:29:16 +0200 Subject: [PATCH] doc: update quickstart guide for new display name (#5193) https://github.com/leanprover/vscode-lean4/pull/521 changed the display name of the VS Code extension so that it can be found more easily when searching for "Lean" (before it would appear far down in the list). This PR updates the quickstart guide to reflect this fact. --- doc/images/code-ext.png | Bin 19634 -> 19203 bytes doc/quickstart.md | 4 ++-- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/images/code-ext.png b/doc/images/code-ext.png index e576df0be84f7f577960d85a0838d4eb2f3cb192..31495bf0b2a8fabf76b17afec5a27fc0a06b98aa 100644 GIT binary patch literal 19203 zcmaL92RN2}|37}Uj7ljLNzt&flWa;NL`6ncsqAcJQz@xPnb{Xw=dZ|}KhI=oZDC-1SD!>;d+qXC{G!xVI*&*vE-zjNYfsBu=`4SR z3#UW2?WObFZzN#rHbY*ho~LeXwNumG!!_`ON8o_wAx(FtA@a9*(FyOFd&;k#dp4%^ zO6ffadC9g=2P_Cey~T??s>zsy;t^}!_yN#+FreB zES{_#;cGg4_{27f(F+Az>*;y(uAbc9xn;AXn!s6+Ei&VGOb)&yk2byMx<4!-jnjZ^ z>}%Q1Z=23mW`1n??AUbXTm*@Xs^QdGrKT2Y?LBt~svUd7Z=LVT&&p)7WxD7uJn$?g z>MDzD#NMOU8f-!*Jog&+PNpvP`qzE)J1?sjxS7SI#%IyJt3_mZI&JyHjjbY)Itwlo zg`!hM}x^y~Jr6uk|S2Y>esvkW_RQ}d1a(=#iZny9UR*s%x|VL`}l zDacBbHi-YCisJq79ZJiK*KJ6o9W=zBO{9=8I((DdR!;E(`49!eP8NEORvO~x4%%MO zusv^KW~Og$OFD0@uV<@&hsn;^)`&?~PVtKR!(Fr_5)(;I`rI}9*0Byd=Y5UKi_^7% zcN(0I9zFW-tmA{NNB^EIy0L%Hru|Q<=bk@F`d!rAIrUuq|7`IuVp^}LL$hE?ptsjq`kg^%8nXwPWdmh!QOS{zGEJKZ2}yyK{}Lh`dnj`we8 zFB_IpyjQ(R+WE?2ylOV#rErWGOeKgNeqq;D`xhKjy%j$EHUpRXr%Tr7czpf*wAvlb+p@hkRtF^oS8Ym`M>v{3 zT(^;BV6dyte;%k;8zEk}(CH-Dmm#tCSH*RypVnMMgjqQL(Vmq*p)VbmS2Q?kH>?XE z(9YiptPw)YRG8*?ugo!l*H^QE_8EfI~gqcDTNJlXTM8ni_AtFCKh%e}8P# zJtJy2(U(yxk+hISe9x>kGjw^aw6s)6Sh(((O%KnJgiY=qvb~MAVyfTkivtUDR*p%A zaX#hP_2_F%q32z*uRn7`1wW7fN>Dk-ckA(tMyztQa>7tc#-Lf7L#NZExU-APM(VQ| zbKT>EDFqYC>yd$h50GwUmNO&b4r zHm>IB>Dm2)r?`7@y7#e%$I05s&Z5w$C?;)fZA&XFW2;T8V=Wo0D_t7~pB`)~oNqPF z&CR`{t$j&Zxt>d>D@CVZrroCYs*aB0ty{+?OEx4rJ3Ajge%#(PGu)iY=&~}utvjd7 z^|-Kb@L;6ddZ0^*pPx!KRnLnR4PIk)VOjZ12Ck-h<9mFKc>!0hl8Gox%zPXe{ga%Q z@l)INiy}j;cC2zErSHLm2gR29{5WqE7j`b(?Z^-4a$WIGPe0X~Wm#9)!0fE)k*;?E;c}(5KJ9kd(mRz+gN)9e86g$AJeNkC? zFG|SkAiqq4gQ~iEhW+%d`LUMs4i3VuuCBzBcK%x@d(X8tKGIb_Ni8{dvUtURJl&v% ze*2CcR`>4pKO{dAr4Ym|FVD)(PRYT+F+bk+wDe|_VQs{v&@)s4@^cmUos$D~iyZgt z->=H*>2p|A&G?6IQHuKH`Ij$W5+6V;M|o}S?wGo7xI65MKb5SJ*Gy6p5)#A~+HKtI zC0CY5QxBdtqE?Al5};&ISHDTm(R`@#`**J&;iA3c<26gOgT%|i?K-3JBVG)`%GW1K z$r<~K7COJQwXMXNH@9xr8Rv7j_u-#r9i*bHEOq4y^=0w7eRytn(HS}l z>^LeWaOuG!_f96Mr?TM91qB6+}760|RgCjOc`|PsGUj6blPm z?Xcl`v2wk>E|F}fOk$&m<=o~Srg8T_-fUSsvqAf*^aQK<>GsZ61!re5Jl_7Vv^V-f zEsCS>jW&G`6`YK7OD(JNfRWf)74EyRpK&6B84h8Xvno z`eMYz#f{stxi;{ab8Ux}!<&P+v}8<7PRk+?yYXoxZRH3w%)>kGSrb@|| z(1(QG)(g`wUAwkVLPElMsXxdW-)9iAeDM4C??dS>%k$&a54VuN|L|celYl@#SQtaT z-DKyO%f*;FY6gZ&*mtCOrSQ+Kts#qx_RL=c-@Lhquh*xR@wBZ+ezBA7KGHs9UBljd zC>FK;<_%qXMuwu2hhkoETUOeP6Rz=~pgF^f16(~3P7{CJcS}UQdnbK;06pPmPuVk0 z%}fe%a`OJNBS((>5bSdPl4;zqhXhXYD z$iy=GZDP5tUazW~;LmjZ>NgTD`7?IdTP(A8)>ancv6Anvos@aWP+956%FfAIs5g4r z@CO6Sr8l1*Q_|Sup#?ORqO$Wg)>rC`P74VM@j5R~Y2BYuPHHS%UmnGkdolWId zuZlnabeE8*C=Crw%!kWpCRml`%-#3!qT3ZOH(3t-Jc{@82n{_XCntAJUEMD%?9$+m zaEpu7n=jSt5heKMj2V4HoT3W%=QHuz8}Csue9Recnm&aF!-I zo#AB0(9iO4l>|0fpiRIGj zs&h|I&+jbL=8Y^)PEIy%?()vgb&n4XZbIO?_o0rJ!JrWMK*(WL17{LBSSYv)0pziHVCd)jR(_fCa_t|PB!+{2Rd4V$ z*M0r+ytX|1kI~DB;f<1>`zLOEEubVbP^IOM3Lo!x?GfbTZ9H=?z_ZbFy}ZV z{cdX`ny#wq{(*r3`H1{9=gyiB0Sl8|kr>FY(H|@=d9k2kv)}nq8G_5Y*x;w>sW700 zHIuVDyM2R$uMd)pMiz4O@*0Jg3=9o>dwXpZsAalz^0}(xANSlc{QBvBw)0`*YvyCZzNrIgYrN|@UK|Bpw+m}j_=p>> z2^F+K5A>2b9uN@l?%ligsnvx5Hximzrg=xmeh#&pymTlWG)8>hkg6^ z>&&*~O3?D?p5Wtq-P3dHBnOAE<6ky*c6RyQuU*%c(=Zicm(-M%l`T4dRafu0apQ*T z;ve#pCr|Ryd*9L5e;pdS<1BD)zzZWX_j7U<0&`AeJLx{5jmRk|Y~fyrzI^fGdz6RdzG5xV-!fw;D?HcP!FApoH?5 zhpTHPH?$`W7nhdmlC=aQT$hctb#xpy))qE?ieM$ujOvb^I(3SdZl}GyJ+E>7iDSo( zJ*am1g+W`+kyep~_< zV02x4Xc*z(F*0J(nq!grx5;R1Ve7VS)2Oo9=?X@UBDM&JfrDaVV&+S7uBDH*{hjRE z$X|$73KvPcU9szka3#Cy=6H-q1_|dk@ez*Oot&IDZ`qPMx;gixfWVx`FTb4l1AImEyCSPj zIdA#m-@JN{*|{@$^U=rDT()EW4_)tnIFz`p=tyFse<#Ne=0S&Omk9q%YN__Ef*)9P zlM2(HZ%Fs6+}5i#)%o>XD_DVj$I-Ize|RJl{|d$b(8vFWS3cfq^}l(g=jhw*R8&PV z7V|A7ZY6gw9DV%j|K_3p&(HtML;oSC#2fv~TD4h|_dTTUsZGhxr;nMQp*W7->n(Hq zT%m-Tni`%yBL_#4Ob~$YZPbx}U|>}z^W)rMmdg>B(6D4;_Mpg$*OyJ1Uqwo|g!udK zBW9{v(wZsxG%)d1HMR0Qn?ZVQ7B)5tyvOp~DCxPQjabK2LI)NS>Cg$MFrImf<>eYvu$p%9|qlH97(w&#AtE#IH z0^jQC>0MJ*O*3v_K~+8}z4@uC>NyY}<{ibSVwaWQ#V(>i&;IF0mX?+m-oFuJYs zfhU~CZmpW#zkmNKaPJ9L))=)Uf{_7W;?5fj!aF)Tm>sjJ9g8CDIvt))OTSm-!21AF*A-G~|GY& zw`3aA96EEi8xZHTg9WJN)7^{)t(nH}8-r3y(NWko6|0$D*Vb8InIAtcCKmSkxU90O z>Q~|^V=eKyW`7qBOE}Z*-n|=d{=K`@eG^8I^K6YE(F37kylph8tgil2TKW)biDOQN zkub4}xCoWFOL`so_vR*gapgVjc{T*EM%f%IQlbAdG9n*(#_U^Vh?fo8C@5nrKJ_I9r`p-6FTbBVRZVIfdSbArTC-;k@G-l07UwWQ-9>S zYoUa!udQ&D9wb;VNS*JSH@}A#Nb)M_QBe;d1f_QRB^4Eki-f<#GM}sk{@FuMZ<4N! z0e9iT1wys}4Ts7}j!_mWj&sHmuz z0Tw{m8(X2Y$IhAu=ma*Vszk(Ah#;4@#ENTYHER%0rwwZ3-k;Os0|i)>^%6HHPTr*{!F5B z0>$?2$FTAnYm;vBR3&_%kWesRfhkH!ZElFaESPr_B$OTWLL>bSB}r9Pb>F^yZ08Ek z48_L9rQ?D5ZQ;br!N*<)1boH*_b>cAmm3&$LswS`Ee9nIwSffs1K6dnuMgC}hmn!z z_0+D$IK@L4Nf$0&yy(Z3mc*gZ+yjLuX|^5hVwAxm(sg-wTrpllOUo}fSnk%Xx0R8) zsT&OwTQMZYAR`h(2=5>!E{-u(OSLps7b9zfIf4r%LC$!Wo2%g71BaOf>Hzt0s z@-O~vxU85@7a?rpA>p#j#{LfXntro%GfI(uTs7DOu-@$-_u>BCEB2$wK)wqhnw6GLap#2hf z8`nl4E@p*5UaOumM->iyI5QL?h=?n-l5K0bR=p$RyE}i*D#p@0dh}?duj+Nn#1m@4 zE3U2*7A0$EPzS`d6O0n-D+(MJ!U`}3)h4SmC0&_@R?4&OJIF3ZhYvv2)Ob$U$>zUM z;)j6IAhwu&9E~Q>s1fC+%Sprxs+lQif^{7iCblETg?AkMBr6{K3clLPCN$vU1>;AEJ{&8_$O_xn>RZvQD zSb7jKW*sbgmBMN?S2NMRpumH?_23E5jXgY!KQmlE?APfKP^Ode)Ec-F7x6l&+CD0L zyIlP0rj~vg%5Ho+C8=N_{}gF&*@kqSVkpZKrmfa`DuDg}0P~BJ`|v=P5|fhn=u^4k zla&*A`T6|_KdDBamo8=0MUiSz@K%|p>H4Jr`LCGh%rKm!ZKw{N*$LT1aT0QxBAFHp z56HfXUBxb;bHU(_g|k0IFN*XZSOM1>21|sTT0B0gtf^ULnpz}dZ!ZMe80dXmnt!z} z#NzzGkML@!Rnm%zR9nb*-L-8ga#{eKikt!>RG{AASeYo81eOkXME%ILTIYsOoOSbf zTaF=NUu>+-0+pSDn&%kQmVb|92Q7Es+CmpG_xF}*`C=lb-KpFQUDL|ix(E6?6E83I z123^=k%^sRl_{f*fpw ziBvBdyNw;rOJ|`2Bz0+2yM3>>AO#gwEHRskIgTH92P2(@_SBUb7ftP^Rzq3tCJl{}fGM>S zE1clf?QR=uB!UV-W}5-~ZAet*co%8E!)9?x55m9&^Z`=tXiCAy^z{neOU0z(cv0ThhbD%jfEN}JCcN8_uh+1cA*5%+YH5)%m%j1UVV#GT$M zClKylZhnc8&E3{aN(BW4SQZr85t*$>cD?UN1YLnl>sOZWIleq&s(vtUWA7q#`6bOUdbivMDCTHaOL z(}4ceor^JoD|cJcpAgInRu?~9TPXd)YAM>4UF-8X2bP?!MMp>5{oQwFWnr=;I?`~( zdsDB$MnQ#SsW3Ex8Y-Bq@57*N>3h45wKXk-aCmHxw`{wzSxCD$JRnID3`^Z}fem$;`|QD(o1>nuexk&&bGgut6a2va+%(%F4&I z&}B8HsMQm$*^V|*Sy)&Q8y(|<&`(47VME$Zvd_nEG=gDCf$ z96@Zjv9_F4CDPMs%606ow0om!c=$t&NwnbW=>qFadGFaDZ=IGbgNX&G${mun^ZkFa z03aYx*o=N$NrV#m>GS7DQBhF`t}>+rp4_EBqF)P1M)~QfIW+OyjA*qaxr-N# z=ADQ;f&&dNh(YxJSO~dkNnPheieBHysq|{^bal$3=EmD*#wX}MS*|?FefpFfwF7}f zw_yc!?2fC(8iRUvG(B>T3V%r6nm`H|Q$_3lZt2v(o}HZy!eJ%;C3mxRb2P5u2UAL& zQHp7kSL=dy?cuA$_**4Q`0$}Hr6AO#OGWf<5;Z0%b=mCfENn@$CbML9Ydbq~?i+pk zFz!Mh*=uUjW47BnIOsG8k)ajG<2E}b`ibdwm0HqmUF^w|CjcCRqRI6MDy$!pljSa5 z@=t~gl*8|N$XkZ+B7%btf}$t!_y2Abn1Zm`GdNf=+z_wN%X##1)Hbj1z0}lEe@`Fe zy-6a(RxU1YFg&!xpToA0+Z(Wfz`2E8mQPz*S^Z}^gN^IA`$HF!l9EC}nH34oJbJWw zexidzz>;{=?_&)qI-<}Mg=_|PrlqB6x7f8eHts)k=ny1sw8*~xew}8;b92IH1_}fj?r#r!ulI|!eDVJ7 zTiu(^P@BkfG(&qcavzU!HIw6jUw^l@rb9_@bB)(G4tQwd{@P-4n)zr<7-R3OkbSYg zu}+u++vgXIy)zmvZ?E8mo8{t3aH;_8t>8DI$!nGEz8rBnkU@$sti9=?Qi0=-hCv=4>jW<*Gj98> za#mrUdD2TWX?=r-+&xDqdjy@osE>?_E!3v$a$6#;14O{d`jM1c{5&bi^o2%zS($Y4 z>Wl(JWBdL9^%EwP-7}U=gi3@B151k#pC|H1Q&_r!@Uo|juHT?@`xF$25<1zp*T+Hk zVj70u0Lo(+67vGo5DFn5y*FVZ!*Fp#dtPOV__!+|xL;t~G`K?s+Iy$#%D6~s(cgN7 zH=&_hx(5czp%<+;Q}ulF7PET{rzeo}`mt?CA5@>$AOaVdw|;Nld2&Nzd?bf*36w-M0suwp>ZLHugKsJzUgoCZ}Yrrq2Z+xuUUg zE@X3VTK=PvcjHlYkBaF}8z>eN&>6n4t%y!hNe5_jkglVgNzdL-c@qv-n?GDXudU61 zO|iJVYz-TWjl2vU)ARZBW1^zi!S0cfj2P#PyLJUldb%tR$LA5yAuFpNWl!fV^ZCn{ zJb-%ou((O+tLK2$|Lh>G!?6T|mB}&h7=j0xl9KZ4*RQCCVWP8cEY-TviP*B8_t=@R zuy#n$`~(D$p&_IGyw9gGUBxBX3wdDM!OTz>nTNC0dKb&+j59L5veG zdV%MenWrUI#`qJHc)Er`sz2uB7?yeNfdl6E>eZ*J01ico<02vnI2U zyL2q!k&qy+NXDC<`3cX(%a`LneDH!IN|^6AZ!(c=2EK2)`Ro1F!nOIfvWkifnDdSe zJi)=iw&Sh)W9n?rHo=pgMW94QMdduUd%z&Z?olEdrf>^(>PJFbmw zL?k|*+Xzw42n1WNRd(UE2^p&3=CL^xDD}#eD@Lm zkld|P14-}SGf7As0iuB?{y;wVn51MRO2pUKmk40M^Ocs7*?dJ)Qyw-a`t66=>-+}a zKYjhW4H7UKpX#L0G^Qt!Vt}p!5$@!nvxH8=3VX8;SnX-U`P`1^Mm2&cvCSg{t%svQcEIwtKVgb(&lFMV6k-`+A`(`H$q{= z?Iha*a3!`fmT^y)pWd55HBfz2u3dYqo2u?Xd#2@CrY4e0{^#mOw8(C@r0WmOIl>~4 zH8!z-{X4b4=tM|46@nE1bz(peMj_i_oV(U!KC` z>z!-9q24sCV(riQm~yCW-ray`gz@a8m^j<&WC z#41PyG2j^A!-Q$zsDd!unA8wa1YZ6F5rpKt_~&WWEKm?pZL13<8v#@^wC|J??1y86 zG%}6$m^OXT!?nXT-xQQufre=f(rImN&0#Ry?ovG~v8}N;@7%fb6BMD_ z`Z6078=D3Rh>U5jxYJHRJ~ML79NMK<*Kn`n2U<;PmwLQ3&Tqq3}VEh;v`8yZ0t* z^yT<*$p_IMZ!f647t23TT@aZ!Ft-9qIXyKMm6-S(>IK^@uNNI(Pl#5mCS|wV;itO} zE3aFanpR^Kf{{1`g)95|_4TV)4=^6h<7`t=^(6FGcX^uE9M@!XkZdEi`e$G=8uRKXn9-B}TiBMFW{2Sse(SN0C*-W2SM z)f?#AJ(_0mXxaL=t-T|EY?5yI75`_gDZ_s&kZVd<-RKXxp|-y9c?VCXm+%>jAWWWW zU7p9edGw<+o!{4cGJg%XK+w3Hn#SaEXiF}k19bC9TuuK^eDqbCN^V4Pz1<^t$SqpL zw1=wkuOwkBzk}#8Kx(e(vYc z;&#D-#~?0+wwdDaF?4jg!>)@xhp)>V-GZ>gfZ&lEVi&DFJOrh9ab-nNW0SD+A}`cV zLR^@88SRn`@9r%2L%4A(df^lJbSO}i*;5Rt=PzCmeh}magdN4_V0%M)1Dr)TF7CsJ zozO*KGSLZ|YrhCamj<(&TuC1<)LDEU^?tC1=dNzIE_V_XB>gd#elf`b?+9RU8xrJ(jqAWT~LYV^9(=gyfHaAwYuE`SWlR@3@nnhkOpR z1bV``gGbZYaoI!z0Nw{jhNgIpg-ip{5;*MuK?D-GZEpSpNXP$|25e!-ZcLEn!5T4q zJYT*vK$}8(b{dA@Pp|~P168P;QgC%E8ygjt!xt44ViFU#qg)AGpl_0oc74XY{UXF* zm@tS=`am3-fRxQr9hj8jL}-~PK>ZubZC&f-NNFIDCk9tcIdJXIQ%1M|Ou#Alf#QvI zCm6q#AkhhliJu`J!)byE7~))%t)B~>9mqQE`|n(4U!pudP zNhPasBz*4cyOV9v^@GS3Oigt|gCj&fq**7?hc|tMZ7@;1Vh*X&TP-QshUY1OI|i+) zX0q%{hG@te2>Wf`y!m&w*&(g$yU`%0_o^1;krG7+C%yE!jLIl-q2J)rI$#R>^DW%I zb<6*D4?c`Y>;6xuhiD0K!Gl-^X9~@9cAl4#dY_P>N7U}uuU0U1Zr#3ZWoK6s7tF4i zk1P&YJpF3Y;T`s%M?}9TQc-Y4X6(j(^8pv=8j=g}^Y^9=H(W1v&O0SGnoJZm&{@Di zRS^z3cBL_u_jb(;t z+Yd3d#&NCe8BK0}KH}jXxMEloXcRQGw1&PX84#wxwY&+|={kEEhy>;?8x23^P%i`# zG?83uk4WfO;7KEjUm#pvKUiCwnd$%Q*EM~k+pud5euUwYD2V_v>XIsgqPnWeKk(Pw zhfxB;?%rKdQ$v-dsS|(xJkrku)6dOiTEcFEK_}m~ z6c^{^2OF#!nUj%svL>dA6o&{b9_I)F0lhiOiP zDwGr0I5_x?|L7F$`X`R*Q)h&2S=M*&(4kP4*$8#l`{>UgI?4k(xVX4fcl}0QRHV!7 z_U#yk9f|?t0ca%WZEa6i2k}%OAcLmB-ta;o+chgCjH{!wGlGc1_0u~R;jVvJSmFmM zg`k(!gybdg!H<+rjESC1P~9CtW&yYNVw8-)xss3Ydx~*n z1(CI3kz_3*tF*;LWt3nQgTISUsVZN)RtCDF$Z~}b!GprW)wqtsDQhu0&r(vZH%g@N z3??)TPtD9In<#(*+DTI{%+Hs%wH4HHyQ??tL@JYF_ijNsE#QjyI&M!w2$XaULna%* z##(_p9sWHIuINlkXAm$6aXEsw!hywk4~^`*2h}hC{mFn8Iv?MFt`RjRh=u{_fZw!< zlYX=^!~CaDS@btofx?dR_=t*RO@ z(~kIh!-ufno_mfXY|I3;F|;lzDlSfDiJxvKAp=B2C}I0J79D{V?&v6jB|zCCZgT-y z7$`1%gM;Au!K2F)#E=u4E~6pLQ{oTtxd#pyoYK)c&$SKDg_)xHK4n3mZ5R9okeafa zydNRgi7d^d6|+B_sX8rXHZ}YAuXIu)5#~XR(7ze&8PbBfrV%u8mQ+Et?78p{xIKI< z(kGfNYN$}{d|SB$YSeOLXhTnIjV#3v#o8W+_pXw zJSha$*^~VSv=^S^oDb%yeC#-2QW#9@5JO@yXaG_Nu`nzP<^WzYl@$M`O*?Lm7o$Z2 z4}UaiJc%^N`;?S8G>9c}#bi^&hat!!adQip1<5A4qaN^`p)6uUJ;0{U&(Bxlyn9t( z8vP606F~6leJ_~$^OIc`d&`hR^7Qh;&VLM$gFK%{YAR2-$h~8noMXFdI)3jJ|NHZN z;armz;lA84G$hVu`LUR(EY*NL1VeW}S-X!-Hu zCHQ(IxNbTg8e$KWJ9eljodUX{3LJ0D>wo-sD`dY%h=ihlVb#Hi&p|;#te80U0im#W zY)m_T0bz=RSZ-MHtXK>}1xFa9{zEgGVlZ?_VBwp%&8lrR9wvEN0t2P)%xDK5m+>OB4|yLST+T+wpzq)5>2t|ygtq3(l2Bx%D;gh%;fMrSg58F-rR7a@ zRwDg{sGY~mj5Q}07r|Zt#T8RbFJ7cTMLMsH=K$tEa(7o$lF8~Xz~|vK6Ca*Np1BQw z`>Wv=1d53RN61>p3#M}*MO|0qWEY!rHu>APi^Ou^JX)SkLqsjhuK{)7qMonwn~@cQL*J-d-}pot$J+rY1JPP2cr|RI+A`hLYj|WIR}*$owHB zpxKas09C(^ECdyVoaXN$@g_Zs{R$d;pkK-#ZZ!ZH`Kw#6_lev z6hA*U^<7)fW-aRjDhVkoEFN*Ef6d0_t(mKyR1FVxhp3QE^*|NMpjuKt9y`*l%JMhh z#%WTg7DZRIwra`|>;||DVm32uYp^eN2jmZo&$V}SgoAKIHJU&`uiB=7H8M742S`0C zAfU?KM2TamJ9|+35atnnlZD}U>O~>7ROS>@igE%Xs$-Ru*dvIC{WZ)z%V#plAxFnOT5X5n+kDPc+o!OnHlBsDHK7GaHY0YW|6(7gr zMVpVORWf?{+)nEHbaxzWR&N;_(N{b~KFbpH!tL0bv+6HIHsWKof1~D08yaZvp86C@ zu;jaErd~Zd(01Gq=_9mldKg(~2XDQWtPuHvlS~{0_%~QhAV|nIU$rcXz9MDwyTnZr zfnj2IVXy5*x(5M9Y0R~VhzJG|TjEp~NTd%+6eYfjBVCYf9})*Eq4DzFAJZUC>*U$6 zf>pr+BzO=`?Yu#z87U7n7HQoa^TTNDggp+5z`#m1(gePJ8Y0dky5`w07^@~knC)Vp^l(BPnL=}q^1 z#lYa#uiA%U1@0&3-i0)bkcN?`(=kt;^6aDQ&u;ogQ0l$e=rOV0cd*&5;Ew!81! zhnsQttn`#wS!K5Vo*g!_Xi_W^D_(=~w`=|Qt1bLnTEvf&><;lycyfDSY3_CvhZCmg z@UR?O8k$wrCN@oCrX!t6ho=Iz4`XI8jwGY=4WqWg6NdKg-TSS!R^31jA{!wzkPu>N z4mLJGb{hjk1ws+b_)F#G@Khh1;%Y+wf2kCI8&XTviDDu~jT9sfd!^&?f!4Bdasu^x zLaBqnd>%W|os8-$%B&{{?P?&Z#iJ~m4EaYRk5WcnDtdVF15g~x{Xj6rYZF&Xk! zo9w9PuO+pMtJ|fL;@*~j%H-x=HEd&^4=ZqvtQ_z^)^uY3&C{Q?+{J_GC(51{@K1WV z_TaX0{z_r~k*G924^JJ~FU@7;e)r7btgNhYLicdnaK&&55H(FL{4!sqXIBH(q1!NQ zTlIT7i)KpKfxj^zBNV2W+BPO2Ja`mE*h4+p}7ikmv{dzN#<(E7rMQ5 zHO%&|9Q(4(t_RHKlGu(w(_nf6!SO$f_VXr^NEDUC?*+glhyC1?qN4y;hnRpw&;{oo z&E_e*kp3cgPs8xH>S`5`8byu**vYWFXblYq$p){YSdK%fBaXo2<_cxsZF!WDk#TB=vW5m7Bw0X0 zHr7z|2t9rMufVscM&bY{M9%ii=*LeiGYi|5+h1vavnjc8^ICVmC`WZ7Rj$U3UBB*& z2waa9ct@)qqfA)A?N$vL&qS-m7uwxH&T$IZV7NY(I76JJ=?$v{()dlFFCxhfJ*>F1 zlAHdPp&_9w;z!GIlG$k@FTPa2180E{1qST+aHHf1dLxTs$h%+fwrtr#D0Dx5C{@;t z+KR*}g+GTqRq4x2+!PXxEm1uo1$3@_P2@bHHl0V>?P`}z=eFFVLWQb8tcxU^Bx<_ey z4?G`&J3;0mqoRKdqUQe*Q4!-|e?;*JuoB^enHe*_ZRDQVBlIf`R|>j90xE5|W53&K7fwpAWMiX{H8Qe|zeA^r`4 zmz{tq2<8Isr}|^4x3lZ)#DNWLS;EG{*&W#M+%W5&dV71{-E{PEuFCQ=$lBEV_kWE( z|I`vNl{m?|ZCkXOg55nNJuoZpR^cqrH((&}Di}cB{r!aE3h4Yqq;014_hOamoTkq}`T5oaQ=W;ROnWVvD4EM|}?|@zV9u>a&wDm%n(?RLz zkB2s1nLm;`w?_VX#}=Na9c)`qF4D#6r`xJr-S_l+<&infq&Ot)k0k7IUW%d#OhNK0~$FzHFX76 z@^hJ(4`ig(VNcov2da2?9zJ|HAvX3xobd>P3%>8bw(_*OpGY0uzi;2SY%}J)&mwgv z?-$HX{W%{TmjK3cJ&?IA`#L2l_qnH_fItGG*rB1J`BuFiQqivU49+#;Ws;LCgWvgQ{S_HTcZduSUeMWhEDz;SgkZDeF*pHGE8od<+J<=To~ ztH!3L5nL($+4mhrnt-5S^{}l8+D>(KHEpLLIcfFj9!VjgpEEP*N5t%z8csLX*IQ5I z)<#N>c6Xok?X%9y%*ly|Q2pyR=>expT5x0}k6cJdNIm4U;6X<8hlbi(l(UJI)$10r z2X|!)+>ODjNV3R?#{RU}+eEDi3NH{)OiIx4)X!fR1E6{(G(Ksgtur*?|R3-}IBc2;GZ z)zsGVSCd|G?77V1r>UvwtAG6@JNxVAQAp{ zI9{ag;BH=V@tTvHshxUAq+`2CO#l8R%|JR^wu$ubUk^ODkUWJ*`0LXKPfwtJWjd$9 zW>W56auPLuZP6a`|Mfb&{QrJk3Qcd~`V}VXpE$AJI@sLYyq{ugW?o)pBIzvmg~FmD z9rRNAg9kCE2VYLFtkEAn+z83(`hL>4SWg%%3ch6IB{Y-?>SBnq@1?%fH~8SY0wSjCXW$+V3qBtVg`l!oq^7kFV zN2=gP+O{J^K4^>2i|5v zLUQ6lLgcpgHpXU_Mo36BkzSEJVuE@E0cj2|3dIOx?wN54u?;I=g&O4a<+lk6jNu|vrDJ3DcKb_LmvnWz=^ca7qSW`RPreuC z3i#X^Oq^lB8Y

{Fl>&rup#H6GstMM{f3wuqHV?5Nts~yz)OE z1Xja4?_Fm+)mF+d9!f;-mW+*7Q)QG;g=e>)cJjFWSdhTjiqrJlM+^3}9E-93V5HA3 z5TI=EH4i6;0lt%A_;HhxoXF%XqaR*G*K1@`^4YPtC;4%i*>J4%oZ!>(WHk5U`UmPo zhk3)~S1AR|^_v_~v9YZ&w2EK9f4{5S8AF@Q<&fKodz!#v@`c$b`0%1)RQnk%ZGNlP zYHte9S)b3fLwoqe)yZs`^>i)j!n|w5_jiAp1H;0MM+((kmQ)W`dKSY4uIIvP6r=3v z2psQuKTsYV>`_&}Zcn&96Vf{}?i|&`g}Oa3706=JOUci#Z8CnkxA=tB6cd|TMp#yM zCsk!?tv{>Zl$E=S|7;1nzP{eNcIV4016w=0NbjAQh9vC<_vsRg&!M44>jOEOHTEd6 z68=d^M12A`yp@%eC)t+P^=bTG=emZ5jUc zczwQ!=TL<4tENiv(&-b^aQhCq5r_RpKlF`%Ct7pqz7DcnA%kLT{C(kYE z$2oBrj$Aw9rO|)dB=w{Ekg~pHD10+k$MJisB?ucXJK|8|c{D|I$J$iQftLkunQ_mr z>FKLt#;|&~l;q>BNy!^oNy%q)bQ@touJZC&WhQ+qLDZ?~7Ng&ll$0W3Vm?+>9P!ac z2W;nYF;#lJF*T(@$9pl?oxpPE?p=wllbzY{v@|kycJ{Hcv2xB^O|E-S$vk&&HMk!w zz)fs#YYSLd(0`1Ly|aGgy!O|3eK1c^OG{c%@OGN_IV~e2s(NE zwZZvfC zl8OqW?k}%C`umGBrnIyOhlGT1y6%z_h6cbAVR73xG-Mv1wK$ca(yDdTn{D(u680SX zp{L+-+-A{Gf}y6azTbi^yW5OPHn+U&uUudR7Y@Vx(rH7f!(Lii+UWdn-KQ?)YWMe} z!}Y;WLD zC$gdA|oVlq2+#WD&ObEM*g>9#BUhmS@c`(J;1fwQGdwFW7{9RMr+L{r~-!CxmUciGV_AZ_a zbY4`F?gWo5m5>P;hV7AmINgnXg+2LIm4E7p=@u$UTD7u+Pf>hzHD?@yMw^CBLn{=L z!02dfht=MO&DCL3*2~$OE3)nF?H8KW5iYY{@z36du~rwsl8t^Y{cC0>6|Q3z%cndm z>lrC2sprwKie`g*#mxC~SA2A0V&_zi!`b;}aSbd1So7w)syd!~D96Xgh;KWY^-05} zSGL_4%Adf$jH05XratJPPTL)n71--$>6_c$_8z@3tb=m2i|NSYyu<#B!8(VC0GV!n9 zzmui|aL`b$udgX7DUl+QlS4{MUfJ2%MSW(Vpzw`|h-mU^@b~wJa~Q0$nSEYmAyYF$ z`>mjW%lndZe0-dn>35PH$7V(T{>4(XY+y);VSlCw@A+Dm=kd5nOiYZ}3I*#@%0< zWd*K;p@;}vpJtW!HaGjmYr6-Ld7t`n%(#A-^|?ubdR)ixBVX>%UQzvRf4B7hk?V0z z2MGfqk$0inZ4*S-+vHvGOsng8X>r$#+V!rA0&0D!e0KKsg3qI|u&|nI99C&wyr?%A zJ!~Vgd1=2SCK^WEQEj)FJ<|;L=?R-T4x0aMbaeE)4~bp-w6*PPk{=0NVydX9@L%o< z&3NqarR;rd@Hk=iJhcr84VBMVI^3G9YL4$7E>IDNwKMcp{?D>KF){HyboA)T=_Vfm zm?SN2ZFl+j_>z;86R*fmHijkbg(@sY!y+Oup}ST2|H2Slrx{bay`| zp-p4An$Wef>e*Xt&)Hlb%EzXQ-H4lz6BE0aC!2P6Zmh(>@!uF04-XGi&;0M-pVQI? zRa#BXU}4>MoYK?rI>L>nmNnjA>KGumbm%pxk^%k4A801P5gXr0-!#>U2mMn-J4 zUf$mPB_$>Qrt40MQ~f1G?Cf5xtgN^!CGubVV@35b7$HXUlr2D2E(Ld zfm;fr+HR8Og;>M>#l=i0C@7v+N23ZZidp@vG`dc4&5}$FhbkU&1@|#9M6&wjl$0Db zynp`sC3tyx=@nEf5Q!O+pbxS=vt04GBYyrPf3}cZB)j_#$H$dx3zWa3rzZV@7{TyOuHzAXL2o{ zyWB@dH-H+eS??MN>z+)qEBAL`g}N4B_2kh6W=%~^c23UT;h?N!*SBxqXz1w&v4)9i zw4ZHE<&HAdjaTU0SWZ=MU0+>{mzg{=GBSec7X111CW`pfD=e~$x8_?uhZy%Pj9NH; zYjVYAt*i@RR7IaL^9POYDmcAr;FY#mY}v_tIqc+=_#r2U%GcL7%H}{@&)Ql>T>L(q z=NimE?~U9`HYVY3fr*LA&T>*pN@!BjBp)sISCV@gHTG1W9+8P=$gyrbu2v&rW@nFUyE9R4 z_CYX17us7?-xnTM)0Kb!x@Q_Zo^aV`hy56>C|-%%OaUa40uvICNxQq;Y%rUdLdkp{asKG|`?ELKD&LZ*(>(XLTZ3db{~-}F zpa;1A&=(|UHx@lSW?lXyqrUz-HTujxmHW=`QDbc~=CEV_JpFCB+Q~|*XIxxQij*ad zjHqa7Xy0W)5#Kpxwcq^Kim`qJitJS-{!o|fktxzv5E&bEe zgOUzSW`I0VG%IpSgQG4DFlLF*jrYL7!21b;^V8E)_YX}j*cKKRo}QknrH1#l>YS|( zee2YS&>lWCp00IrT>E<~K`J0Gk9v7|nV8Q#W^PV*+t5&1NeKte{V6pyYN)7?xOh+) zn_F?0)8SfwOKYn*BNZwtDl}bswb{`V?QLp+LrV*-pZ`r(J*rS=s2Hv#?QVE3AV8+5 zs7Tv#3Md(_&0#cCk(-Ms`rQ1gZESKd#2;sG$hRpjr4uC_4<}`~(n_N(oU9M}x}=QE z!@GCy!io8g6lu(sIMko5B(dU9^IJ`@dY{gtrh4v+10Hz7Zb{H|bM5h=eRqF96FNct zekc9d#Kb-n@arNAI(m8o=q`rF#+m)5ro-QG;T=@0tTa7-0!~Nl3tY z@+2R-O1m8p%h}m#8e&2IHDw(eA4jYt11O_#`iMamVYG2QTn75|0R z?6Jd2cVs4ww%5@+^$K&RKAru8)xJEFzSOGe06{^)u?7zgzyj5VW&!^GB_1c+8iczR zG8*1H4JWD%?rcOH*4g#-#Lu2RgAY?RB=0!YsH>^HGW>&y$DrNq}A+ zbOjF$DXLp=J_I}!{F>$OatbX~S57*Qi`L@~Qo?Pzy^&;1o#m0901Y74lQkSoae zCK0S%!dTOtRCFLLj(+EMv({Xg+JaMzit=8X*V)k5ZZ`p`u$st58Y5tWu5$n7f`Q%q z|A#XE|FFdWQpS&g@O{3o|4SLI(baTy=a8>T`Z9z*2{XW%=mq_cm;bN#V&MZT^~JP< zBVykBpAY^gMXi>O$%MBx3#4ppn3qpXJQ0QALGu?3bQL0a@}$4aL>4e_;?(!T!Vu`i z3hL@~>hZ71t2aZ)1X90!qbpZuP*zsH1OOWqktX1i8WV%#ezF~^kbmj&*)^U~3ySLE zK#pXn_2TO4r^rYwKKDaRL14(+_W?Rk3kakE`;1CV3|23S6V}wxNxQl@DYKenpK)6y zdBMPN)9}>V(o#x6;W11QD}|O~%^JVZQ0dRO`!`oRJ_G~=9$+L30NeV8h8!p0 zTgCtip(;CUPjOY+%*u#}pa3X=`fp%n))9weYQyeO3UE-_g(kgQ#sZ}j+8*GqCw%U# z(6lf{${HFPVifCoNGXenKts7Q zDZzlK=;=S}_*~&4BO~+j@@B_xo*!*K;c>QXxZt&&LqY;(6n&@h)ve;+y}e;$W2z)r zvSMO?vFf>Hk~w_=szU=r)Gu{!uNuqg+F0o%_E*+ZoGD%aIk@Z=?f~u+Wh^H7@CXAV z_D*A1ZE1DMz`T(I0u z=F`&G7e1=vLz1H)4ty044^Oksxv1G4ubkL&|h$7uHM&i@|&p@$5dL{(jVVR_kUvc0UNBm+*} zatWmwZyx%T&a5H24UkN8OUoS&4i2Dm2w3AT3oN)wv(GQ?4O}7+Nsj5> zt}e+{uIhI)o(Iyv<1)(r9gXU&!vE1%I0(UO#_MGIVpYb>8b?B?P_ss1)#df;*B`t) zE_xjL`0^HI^64+TyQM%ofms9c0_&##uquZ}jsk+SC9+w#g4*I(>pDL_4^n{L;hKEo z<-TNF$deBR1qHp=p=Vo5_HGUG&Va7qP6IqchXNB7m-OY!?k{wvh%aCM00=4h@k4j% zPb3Wv8aGVVH80==(9Esjwuo6;7A`5&Y9|{Q7(5a1u3wtqa@(hbgGH@*0ds(Iy#TP- z&@j8VD<2TZzp)ZzSy@>Uiz?7Uj;3g(vGDQVLO+1s&U^S*2;drPjhB>E$WrS42M;Kp zKfepb6Zmsdh^FbcR1}5}Nj3L3C#@Nn$Xk|AhA))Uxu{i?ON#yyGeY{mfxZSvWGK3mtcjRWHhWnWZK z(62X5z394~-EUw(;dp0O7AlCHlT#}Y&b75Q9{Yb3LIJj?yLuqeA$=_@%&x9hRZmMw z`t0lbrs1l)yW4ay7bA(oCO0=%wA9vRXGZ#DdwSE#MpyS|1clHTOoP$4`a@1vl9H0p z?1Xi6$STwkggU8QLQqHuF-<^!IdW%!y7YkHxO@g}2)eS{Vkk$p1&~5E5KVw1N2jFp0PxA)|5jM&IagTeLl0V|$=Uug z$221yU2rO&M=%rn&He5q4q57!-CzFbj+-OW_7q33^r6*bC@-W1AhE?nX-lYkoXS(flW2>fPjDyf>(aA^eX!>Gm$I2 zk83fNp>{$)bDwmo2lmHqJ$3IrG)*-%wFgg_g-wzWq#5)|ZkO%urH<(Fax?6U<1L|l zrA&oz@9KapLpn$(4dgjl{LtuI;T zaG-{jKYS4TtaKXvjvtR0NCRYEhgcvLAkGZLlJsHopzv@LKs125_CTs(BcP*yfdHD- zeQ@#279%eZl^+Bq%FuP7*&r4?ItPK;bS>jQaMbj^U!D@P?c7h}PxqcJ{D15bq)41h zJK!TFRaH$nk91)f=70P4n2iE_j}wg+_#Ro9dp7GV?l8sRmJ3TG0PGdsUR2a$IJuVT zKvV?sz4eP4Va5DkxO&PX?Q}~tgEejnfr;;&$hFu|qvd2~F8E4%P{I>8VpukGXd;N$ z?xp?5qxmnQ{x66oU%~dlRCU+x<@q#h82@=H=(g|NjGhI}VwNq60WX_i%gw_bV&yWs zFIXi1a5G=RN%1X?v9V#v8-?t}P)yPKeE4TyglX&h+O}_9x44?&(R<82)R2y7>d%7z z?}`2w=41BL0_5L)4+?##vWEq~6)?`!)YShD9wTAsO676g_(z`)cQI<04LS{(VQxMb zzSQ2IuqZ~bFyJusXhP(!NKansBAHj5#~sVl;Beq-KrP6XP7;ODOLFR7Y!5#GrSRDl z?al3#?gSwKAJBww{3$RmrLVs)PZA&u2 z;$dAyUIGGv#?qV>&ff{g6!t~G;j=J19_CxZ3znr>JP#Vf$In4 z6bb@Ns4V}P@PtoS90LL+16KqKhtT`#NagwF-ZLCngp+{T{5)dDgtMeo9Z9o%16;5_V2T2cESXdZrtdG9F2*U=-f~fk=)>deK zJ}nZ+UjSs*{@nn{GSJiWm3p29jnUB1P;67VQ1y+RTm->u++9LNn$iY0> zEad|Eg5e{5F$M;P8t=n8>lR*q{#0-~XS^@0^ZDeo7oXQERBZUA03{He5Wy3w(k`u-R)L;r9EonUuwFTctgKsRV2dm9DC`hcWB z%K@9}O@qPTKWlEHqIZG0Cmsp{)mn{J(Z)hyg4vkJ(s&4R`##9XyP$(J>;8PNfoI!- zpY-T1!go2^80J0bW&zfssGuOIr$+%eaA|dQac=HCj2~PqOf1%mYQ7c+sm@q+a zKHMz<0Rh2ILAqU=Y2bls-NXGIfJ3hhh!Q}ZfuLpnMe%DAZ}PrMyc{!uO6+;L*Y3DA z5ew!3i`TiMaz z51|EsBLwbO>-cyAI2mDN0w7ujeZ3DQ-t_)c?UQ+s=FnA&wW(lkEG#UzPd~xO$DgRQ zLa6KGRW@V*_%hi+eRzLy*_sQ&F!+n$fY<`ZbHDwt;^DPqJR^{qhvw$y2$&M$b4;yVMJV)i^m{Djya_m zrln{ACAhIxk(ZATg#DKGb`FoU`g-2)nl-aqS^fVz3*c8*S9ch6ezgR}8Y;43yoE@? zV`u?G?=NXIZ<%hV1y-342ZLuUAt`BN)&#!c+`@t%tRiT$Cl%!FuI2=bw8(~;@9y96 z^9WhFu2qD20Ys;E`D)|%6$=Zt6AcXKiDU~dTB}u$msVBZmM0d~f9m=UCKRBmBPYda ze$WgvMPXd#yn|e!t%8f)b6$Al4(he<#2XoeQZq%31vaoyj>7!Ef1Z*D1i(KN{rvpy z8gwF31h(PAm;1|I0Fws*)fv~l1I_FuJNt7AiZ??6h)>I6jha`0$?yP39tfhov9a%> z@my_fUxL?}Ea0Op6@WOW^7l208w#ai4MgC(K%#ro z1Y`lQ|L49}&psu^!J+I)ii(O7gyIaw8^-w`bTl+h+qw5Ye!|(k$BP(m9~_MS`&W)p zv--7^)PvFXu*r!Dz}tR;8R?~^QD7-ep3{7#ka=`<7KYna9;Pg{Y09AP|C;>NMQs7B zco6KO5)#z<*fNz1I=Z{-S2!Ky@azfY`{DW~1`-l1KKf0h-Ve^NVe{mRnRwu0qUDR&QG#OrFs_s&}r zdXOxDS^uZE*BXnXlsn^n*es>Kc{=&?h8UrE$$JjW3;s@KQrcdT!GxjzIp7OB1l5KD zP~&-K|G73HI~k2}MP;D1=i{DLQU2F{G;~D3MDkLUnFS%#nAvd{WK-waSg_RABt;}^ zy!o1iCFI%jpMlW}61aD0W!1KNQM@<*y}-2Gc20pd{F8dwu4~wTAjw;h>O?Z+bam4o zKlRQV_iFs|wG3ro=Yttla-;HfG5+qOnWO-P{H2CR{MfSTbG}#-LPF0BOXK1<*=b+h z%1I@C^JeQ~;H+6N-SANyAFe**i`|QNWFr3E7xs9#xXazH2TfnT1QUPr%kAjwG@PEm z1$j|X^^5GzC)D}H#o4uE)J&J?2wM;X2@j8sp6rdezIajir(4WqD-o$qhNeq2 z@X~mh2hlmm-P=>hMao?Rv-tCiM6XpZc8zrw$IJHCXl< zYGo2&`q|ow@hmIg0Nb_VIKv@66&&bL_^0v03qO^qlV{kbu)I$X`s@M5ZP~0dflYt#IHG6Qdv(M+m&*H>Y zWA3g*$H)K9#VDw;rNFJx3@g?l|L`=xz|{24&y`RMF$r!VJ-u7dYVO>rG@45nTe9c! zaJDg64U-Oe!js_TQRT3u{+yk?@&PILZ4M6Eb>jAL5=u6z`-&_M!JpAYGSCT)mV35AUOT5Fq`8ZomD`xtaxTvW zjvnXJiYN1vjLyCCKDXm1>+wXds11my+`9FWjfMJ3f)FWhagm1Zx+|hO$~n@>A|9K| z^HADrTU4~|qmygkXZ)xjF7LoHlf@h-lgBbx4wsl_@x6nM2CLB35T`j&zSr8;_OSej zI;80Px2HT8gtMMkTnA0p$z#}W{R7c&*(44P8SWn(m`=Ar1@hRpoqbbo@A&-H9zt71 zdO&ha@SE(3P~NUJ5LeXqAt43a?e`zvH#mJ}K)`o=AI1*u36LSdg5gs4;m6(GFI=l_ z?hqC!aVcjq7#my406l);bp}DxQmprqPtAcP>|kYS??JQs#d@%ANh|^x{pC za*5TZJ1naVz%LcG&I&A{qAq{OdV6mn0i%%s=9NhtD%vwI^r_mG!oOWqCjIMI%%imE z%w_zg3}#lre5GIs%(ZHv((gtfe7cdiXbSN=n3#-;hG)sq+_NC-CF{aR1`V`tDNj3Q zqBbk*bJ(qc3?Y-o6oI7A_zJcsre1@aN{}3Yh1vcXb?s{R_2Cf);S}|?(hHSArURd{ z8}!%W;;$SUPsxfKkF6Wbq>#G18DQ>FQu7ov$Nv)0Zt;K5@n}$>D0QUB3-S3Br{~X& zEywHQ7TX_U5sn1GU5s>I=asimVdeCZF~Go|3&(BRcyZ(1teKjykH*Njo%#6AW9EdA zlEpN`uG|V@-XEU=o5Srl46PKv{E*QzG?dz}DI*|C`pa0J)!PWjE;;!{N4l7VRK#_k z6aT6f4+r+EC3)-QpF5Fn+e`PuXJP0^iE#BDGZkczbuBIZAoEmM7}HXgM}#}2-Egsa zIxlc@h%EkdQ8wjgJ4eK~ZxV3Pe@932%F92NORla@oBV9*dyId3#57FK>(~m{Gy-6c~za2eCLGdGk z?2A#$pZfzlmzTWXjkK57B2C*ueb8K7ibYSf@GJZVq8>xFQdVYvK*W#sKAPHqlc0ep zR9P~d^bv#XDVlQnTza(_le= z{4h-EopP!37BlO{L`}*$FYi4`$xWYlSX51HF%nd=yl1yHstQ+Ig0d?3#jzECk!?JD z-KTx^r=#QPamy=(sOYufIsvz{njZefPbNeuvmVEm$UocLo0@&eeCI^(K61lRQE|CM z_JiP6UjDdJn!CIChfP7jU-$0cFQ}?FDfZ@WBHJeFFSMYe`SW|Q4C4y*L9Ba*EFViO zLsAwEEu;Ae2j-xOC(V`52EC2=jn7`r6NYE)D_8nmmB^XHAf(huD88ES3B}LL$u+?S zwC=+#9dvkwWBZ@r=+7oz`BH=^@n69K>6J?-!{X3J^A|NHzAUkFWq=?55m^3LzVstc z4hk@A1fB=R5o+x){|g0_B|@K&>6GwK|po5eHgnwhm8Fv;A!o!tpXZ_2frJg$n-1P2lQ871XM z5a>80TY%HwM?=f}Z~E>fQ1`mjx4U^Fvvbh9S9|%kJ=9|3p7+}Mke|Z`Cih(&V57TbD^$!1Y zPHt|{>q7F)7R51H2{EW;lIK7ZTLJkHtcEhP!RKJFopR(@vfu?hB~^uY5OEZ?O-~od zWA%0QG>?xT$(}6C-XxY-)je!!B^kup1NziUnXG@=k|!=DrMr{56_T`zBO~)2T>Yr% zl;L#p_!ykBxyhT~8zXbGo{V=kXft-V{50sL*oo<6KqbtV)YoWaV zBAm;cz)2coX2!dxw;|!nm!I2O8Z>k-UO$f?%#oC>b=*Q3%003-U2gG5r`43H3vB$4 zbP-=$0iDcp>W4(9%uIy^Qy6iW@nwq%=wB_3LhJr7>6(-0KXz6F>x8ggWL)rB@6%l1?Rn<$bEQup4^+v4u2z#I%AY3X!+nF4@_E91Et0!aJFzrH{#Gk)GZa z2=?`DmL5gctaVL=wfm>H5z&eiT{&u3ko)Tp%kI}eRHGN_;vy0G zaF&V%nSx>zr^EBq`S7rQaY5q8kJ~DXHaq(IVvSEFd5OZo7`L`gCFZk7valdBs}!QA zCn_woB(#+EII(PR84Bq)NR61t4-I7ikT<|CtwsN{v4Mxvof6m$;pOFrh}pk0;bc55 z@FXbrKl}R={>*2+s`_D>@Smv!lpK*-V_?7l1p!hmKYsim=jJBdYI;#12}OX*Wt$lI zKgRc2uzNw;#=*OerTYc}TTrMzfqc{`PJeAJr=ZYX{JDvGKeGSMosSW==afx1$Ik|} zeI7k~W&m2q`b-(q_O`Z?Qp~~DCXAIzek<=dwe`L zW=Yul;s_Nk_a!s4@#=9XNIZKR7CV`8G~@MV3^2W`SQib%#1H@~RP(#;S!voh_1kyCt*9C_0pC9dVbVrUJwYkQ?J?0HHLs-%EG^gwYC!Ak{ z;k3Be7q&$--e`raReNmCn$P?iFvLfJp(1&qMdQ&#xId_m{^{*2GU*!_w0Bf55(_v7 z&Iy=EN%6bHkxX*zFAXy3!7IQnR7*Tx$qHOBGcdQjBqx6lGYS!X0CyIGWDxkf>*3)6 z>cq{f1x-kcgG`X+y^03KPv=$;RE?y=u63K|dS;36;Zo6%s0~x4K~92iUhswLexoYXA9q zST{zc&Y6Vsi3(4Zmzmjppd#f~qZySX>gsz_=*9Aynk~sp*X_YZO%WF+MCraQ?b2$k z9CaffKSqBHaQX$Hxd!U&-!N6RD>htb%YUyX{GD4yMo1H+L{}O4#3kzh$=Y?5w}5cl z@#hc7Eeh(+kQM;&|D(Jd;`j$-6bq0cP3Cb4%e6OW9YBtYq~p z(Sl(G1%;4=gqkoB7nY{gqjqrd4EwgN3^f~`<`kEmmhtFlYAWqa<>neMDI0SXSQeY8 zF42UM27T{IwKnYj=^I&H>o#?GzESO+>dfMRE+G-@RB2)91p&(yjwwi8;^vIr538t< z&QeQGoL;17XrBIEFyr^ zHsk)AsfgXd@17qXohgbJpZW7gb@kf%Nd5EY&$ce3($7qct=+VeXy-Hsp1_@7UlVe3 zd-B}H?1k9biD1yT4YfF@regeKZqV0lot;G?-Gopjwd#%`%T-Wd5zW7uoZK{X4vF@K zrkg7!a1X9^konx)z#mQT_|yzS8Z0pg0}H#lp7K30e8tB0yR}uiQ^eI^XK__zmf7`B zR=JhRq?Hzw4@X4{ww-x?%myN4WZb*a}oXD`1p>`@ztHMy&m{@Sz%3BE=Sus{5Bi_I{2GlaYlKf78|&0wES{wd5lx0Ga7`|+ zKK%J3M$LFkU|vB8=6u^QJ)kvtHF+7R^xv%!Qqlf_eT^;ua%Jz;Inm90PCkq4eCvAs z?t-JB5Dym4)OPM|6(!9;Xt^;QV2k^fmJY1cUECHLYqCKF!5ETd$6M2OADX5EKI1D= z=?P#t2%8{U5CBPua;NLGA%b73K>)Ka&rlR zW=EIN6NVz70$_@2_aih2P9bIIXqo=a^C5TVFt11q4n{lPo|bv7D^@mgagL&(s`}c~ zvygJ`?ZdaDT}EyO#qzSUX(1tpq8@iSz_62nHuPPq>r|0LK}?#D`Yf`>pC;%@s+i+oI^%QLb5>TV5Se~T}7sN$?ngD*dh(C&g&8G3_1{r2| z5cXTh(m^?hvOUiZLx06u{_Jfy@m%M!B;&rxkp6^cicf=CL2ymRZ;tvh#y!e&N> zhHTgVQgp~_s_a2XClg{cP_+;uc3mA01qB5d_mGr034d(o;^NW~tE8at3yjh=*gsHq zyalO22m&u7b{4g?EQM(ejxcOO^G!Ld>-+s-ZM=XiTsHAnT#tOAPSs#{f!IFA zR%AJUM9|43;PtsA=sq5vGF0XTX9t>%d!Tu#mvbD2U!0-XGp;|-={>uLjmYsbYeEau(VmgB^&8}B4-9qlPNIhEWyzI;h!Q?KNxjgw6Y(d)1g z$dsdd#mxNF{?rtNBG0Sa;xhbQF0;LFWOc}hEHqNShEAABl1W++tz6IEfWg*2IT;Si ziru0iBLfSYT3T;0;GLyv)#KRCh_IAeR`cZ%weG9)N5)4RIY_)0|LCJ)X9=vgQy&ms z-s_6LmI6eK7pELT%5vYrVp7BWEg;xGM)vhymyT1EHC$@{rpr=5O<1x=2@C6$N@mSz zJ~q-bYc1<*=nS(WQaim;iHVPgoejdD!n916*E|O;Fz#7OLR3@W>XZ$Z)XjTLLBZ>D zxgVibWN;RGN8hM$@K&<&@`_ok9XP6=t&fBM0-M+#K}&0CX^~S@%qp7!w+d41ked_t z_HHb%hn-+xz+&R!wq8l}BO<9I9o?p?=U zy=P|kb*h4kb+E8?+2UcJ9gsx8MMrn)drKb4$;x|7oNp^|`duc3Z}+ zb>4FC$~uR{A52uc%hNp{tuHGnl#3g<_6`p5 zB<+J;8aVaueWvh}oJOi(vP14O_AZx}rY7V$8j1yTl;~>QkLUow<>m+a=YCWLEMsP- zW;34t<^$p38U4*ab`JllDh`NDHm>S@x}gM%VXV@rffaKY5UISu^XZbsc4D3u&|>8Z zEMA@t;$jhuDdW`7rP{ZbPCtTx4EVv1A3rvAwSD&B(W6ITKhQETK$Hjzf-11xC~Hx_ zW^^0pE$ZN1k4IHXfy@bE^!~QRh`@a*Gr>=Fh5PK1mx<5m)cnn`RQs|FeKlE zg9&SB)wygBUh@ygYq79ILl{|pAKvkIKzIuFj3I(6N_13BOhYm{ur;p}ItYXjU{^|D z6v8}>d%ggS8?1IrBBBBoMY5-#>p_nxm%@tgFdUnl1i=wv?uhL>ke`w-1q-jSY{3$X zjHH{Qs@`aY;|IIau8awh=y}3)TDTVoQV@*Ify;sPEGS@L_**F7)0l-~~a`I-Fy3?2nl51KCEm&XiZpz)YCJLJJ+b3e!!>Unl8o2;))j>&sU zu+cGo6~lo`7O*egG|9rw!%4Jgp5ZgNwV-|2KC1j~=cYWyw+GB#ViFQ4BbkuIKw@Gl z7BG?P!Y#`22cXtH!Pdo@mKXxP6jo&H$`=`66I+uUplSF6g>7(ugs=+Uy^BRqAE05s zn?HE`>Fa{+NlERZ(yw)9-y_)eAF*~|s0MEz>Fb$wJPQwL?eFlV^542|X^9LsNywt0VW#F=UHtTH?g5TrD)ttwuUV^YRufFmQQS@!nkgiorzW818(iZ17`Cwv` z`rHMdWkjUtuXxK3vqeG(IZBLLH;7B|LgdXyn%H^XlNkl&4Ez|sZ=G~NW0DSwUIXIy zd7%?hC5z@C4>_*c4#7JdZ;RU~`}I8(D-;?j92yJvL6!atU@#z#OAaCUa~Z=&Ke zY-NF)5BWXVGAo~$FZXx<>sK0TDy~THt50*o6R0lXBgA}rH4_K$9qCnaX5BN`5iuvjr0ejBGWXowO7MKVhV6Q3L@H^omEs6$WB=?giViyk| zi8Fy5f&BDScwE%!_4TA6W1bcz4QGs#JU!?qxj)F$GJoCn`!Hz-V+p&b4&7WaWqQ8@ z9Pm~@43#mC-Rz^lWR0&Z3i(n(l|n0T=IF#SU(n2G$)(bQspG(ir-W5feN68Vs~{s1 z8qlG~-pVBhKRbZtiuhfCOOw@inM}jE#*=XhEwwGT%hgYHblyI%EL%9Z8YKc4K75Tx5w^W9*HpgEXhLUa@Bq0?|(KBUopDsR?q+Wb80FnVW>KF zliu{yUarscxd#3x+ehQlof49ukjJ*kY%oW}$KYXO5+G23IIl8xkpt!vD)a59H|`!5@j6pMagUSlrtWWCD4!+cJuq8e&Y7!#d7%A z-Ccl#x8%UM9wHOx0x%?M;b|CgP~-AqF_^WdiqwH&Gocj~MKZmeo8XE;2#JW(lXZmU-Q+Vfz^Fm@zDUNcncu9rsA-p?EpY+lt6S4-Yr z#%F(Ct?gqXwGsMRB;>-)H zK;>Fyq(VwQ!%ySkE6tbP7$z)U{2P;wfqEt?*fNbvea$9b3FD)YC(fEEx-%IsRvy^T z|19HA?)iRtbG*GnwZRm=c)H0FmiwX7Jl{-xWP9|h-H_$$@uw8|FaCxGHk{6U#1tu= zajo(!KB-KK6QsC8onS<(y`S^6oUFhqEMxppf~BLNo!pdsf*rp{nF4H)~*R3((ws z@$4kc#$dt2`+Slqq~+G@e`9yv7a6=&n2Ngz`^Y&WJe<(FKWn^yIXV0&_6?{``>xy#W4{)YKqf#Y*=8 zsf0ac|8QNAijwjx$S2TwAm)@cfRs)!?!0qy!N$v52*EjA92^=B4izmet^JEDC1ND~ z`8L>6SqK{mb4Es#{RJstcb^o5@E{IF^bYmCs#*%fmIq;gl-D)=H92|JWD#&ND%cH@>D?qDA+hAh9h;O?(Az5$8XBs`Q!agw zgrsBkx6ey8H@jG+uPl!Ab@%pIazX-Z_~<)a>cDPoZ{LJHaIjA$;^^&+0Os7L69$rM zJZ4%#!r6SE=k=u;)QYHV*f-D>;L@UbF&6r==k{y7M47YQ`413-#t9Nu9^z+UkcL>N zyt(-|PyRIRMo+Vjr%&`ZkbmMm*n=NWsL^CJGBJ@nFYU;ytGlS9AcYir-eA6;-);CQ zg#3mEEg>PH!@Ed@E`ij~pLbeUSr{9O0@$KZ&ft)7^ec+o_Nf>fy)=;G|W0h?Dk`}$N~ z62weft3V3i*G03g9BfM*9vX__=Ha0dhjbVn6H|PTv7)SO`1!?!3a`yWB-P)TY01e- zK0g1s7q*;A^718yb+E(V+}>UxDke4c`)l%auxk9%ZXvO+w;6kS)>9$|0Iucpi~!&e zj`qHX4<3B2s){#9hLH3rY_>f-BHYOlzKz6A+X518EPQ8S z;fwLDV-X7LvT?(*@uh<^R%T{F|68x|CQ8m=+mnBOBuvZ~?gA_|P0bgdewXYzeEOXM2v>XnP|;ULq(AzDw2bkR5Y3Gk-Fzn_6DE_&o1c+E z@g$%Gb6dMu1%4nxg_Bs>#f9S?eA7o)8k_;xC9t&TTJCk>40jwRyjYZ|sOS(#ia|m5 zrDbJdueZD&lImMgJv}`svh30R{x?jwF&+NTa{a#-IjrOVwek^*TR87>OXL_?eKD7m_aJ|5Zb-9&oV3Zs6g+e=(1) zWYhTbD=U?~o6@vzA<_Gv!p3lTA$?`V*#GxD)nxUwbwzpk8W<;sXh^EGEeHGil;W@g z(e8ebtjsSi{(p8Ic<#YVK?aa#4|v$j0#>QIJ?o|yeSa5Qxi@YVH$xcrN8mv;tJbZ{ zyJ-g8v9zn=<09ao`3eJ&S+8Hc0&YoN^7{IE_uS8aeiny@hp*naaUvHp&?D>&IoDoI z`B}VU@}xIJRS3mF?!o&Ny0k^s%RcDS8?dTu$evrxstutx0B;>C+stzCN+xF2G% z+)FD9ixt2qysXTSa5VQjPzu=KT=a-RAuorC;otp<6`7eUfpf*1-uQZLzrFX3>ASnT zk6RTnM5rE~6K(aVXlK|L#{T1r3oO061h_W|Nt=;@PdD~yT ze!X}baJxY`a5EM#<4@ar4cJWe5kEg=$xdOZvl_W#eqDwrN%j z%&tL763=GEn2}s)z4*}Q$iB}X(M4K diff --git a/doc/quickstart.md b/doc/quickstart.md index 013ae908d8..afe06a296d 100644 --- a/doc/quickstart.md +++ b/doc/quickstart.md @@ -5,11 +5,11 @@ See [Setup](./setup.md) for supported platforms and other ways to set up Lean 4. 1. Install [VS Code](https://code.visualstudio.com/). -1. Launch VS Code and install the `lean4` extension by clicking on the "Extensions" sidebar entry and searching for "lean4". +1. Launch VS Code and install the `Lean 4` extension by clicking on the 'Extensions' sidebar entry and searching for 'Lean 4'. ![installing the vscode-lean4 extension](images/code-ext.png) -1. Open the Lean 4 setup guide by creating a new text file using "File > New Text File" (`Ctrl+N` / `Cmd+N`), clicking on the ∀-symbol in the top right and selecting "Documentation… > Docs: Show Setup Guide". +1. Open the Lean 4 setup guide by creating a new text file using 'File > New Text File' (`Ctrl+N` / `Cmd+N`), clicking on the ∀-symbol in the top right and selecting 'Documentation… > Docs: Show Setup Guide'. ![show setup guide](images/show-setup-guide.png)