From ca58efef3fc315c16b339a6b6e609e49efa2a636 Mon Sep 17 00:00:00 2001 From: Eugene Loy Date: Thu, 25 Jan 2024 12:46:03 +0200 Subject: [PATCH] updated readme --- README.md | 2 ++ screenshot.png | Bin 0 -> 20558 bytes 2 files changed, 2 insertions(+) create mode 100644 screenshot.png diff --git a/README.md b/README.md index eaceb86..30055f2 100644 --- a/README.md +++ b/README.md @@ -48,6 +48,8 @@ By default, running cell will rollback any code that was executed in that cell b Manual cell rollback is also available using `Rollback cell` button (at the bottom of executed cell) or shortcut (`Ctrl+Backspace`). +![Backtracking screenshot](screenshot.png) + ## coqtop arguments Use `--coqtop-args` to supply additional arguments to `coqidetop`/`coqidetop.opt`/`coqtop` when installing kernel. In this case you might also want to set custom kernel name/display name using `--kernel-name`/`--kernel-display-name`. diff --git a/screenshot.png b/screenshot.png new file mode 100644 index 0000000000000000000000000000000000000000..1bc76cc939ccbba3dcdeffdf79e616451bda6f60 GIT binary patch literal 20558 zcmc({c|em_+Ba;64%8`2t*wGAX$J*c7eHhWq}D1@1zbTuh#Dm#yI~20Br+)2vZP82 z$`Yy|$QqFyfuJZ65u!i{5FlZVB#?w91QL?G=MFyeJ@d@W^Ub{P^S$36GxjFuoclWG zT>JIA?w^jkIcxoC+n+XU*r4TdR z%z%fF(Fa@)Y}imq`gHBWAHnm+up?fW4I8xEp#ObD3w?BH!v^;WmmdzC#`?{TbR`GP zTwu?8Z%@ATTk6+de_YeJaoyT$VEcfVZSvc<=E=H$nYy(3FJ-w?pS8Vh2>DCZFO=M0 zbU(i+`Ao3m_6@6^>%r#XQuR3Wt@e9ICd@DHdl$_2#u!`VKZ}_^zk9WS%*{C^&cTo| zyodZ^L9cwZb*nqGvzXV2*An*@w;Y3f>Pe%{?SL`rAj~@owgF z=3ZL7>6(fE-^^a&)6gf40tVVa-N~m{|zR%}PkPsQFAOHBNklH2_eXa?YoICp&1`)A- zc%qwFlV)a43)y z6LlgtXHQ8wvtofsZz}b4D|vbGM6P28l8Ve^3@+Rqt51IE5;^ZDu!ebNnz-840S@yeXvl2d@Re3^q$1pN>8#q>2VU$%h_jy>I&+{v4; z>Gr6z!x=Xauf@cUOdYCcdtqj$P%ZtVA*>6=DQ2B4G~)1=6%M6)v#M}zehp=N-FjKR zd#KvVTq9#i{g_lynfdY~e;%QeyqlWG2!4(^qEWjPp4r?KC%=|S@kS&qr#u|s5nOV) z{ZC!7Zk?1~R74)r+KO%=8GtT1f(GvF#!vC4DfV;MKc_0*@EIEOrF(+rHU3KLY%3p&#WzqJ@ zJIy^~#^=V2&xn8Dq)wg^cgV+SML9&{AQ<>7SfX(FKhDCA}V>{Bpb!)7ICRekpL^oKH!x@Tj`%IfuO^fi;diqz! z@pn*(TpR4HboE&7AAfc9L7N+i(=fjP)}H26LV`4-?a#3*w4E(e-Yjbre|72_=O>yG zJSyaUL$jLuBd1=IJ$j}?thyZ%ef*n(sPDX^pD1>8GWD=o7YckFJhr#Je9@XdT4(wA zn9)&;DACet+M( z{;@`L?tk*{>Mn3!=RDBp({cIY{V70M}A)|9;*FKEP?Maz!}_vF$4JRCaGv5Tg6x5CfCE7d!) zldITG^nv*0kXV;bH+sphVG)y=G=)6*>qTvBU#%J*{0r&~10 zNn06baD)2j!zu;bcz=CrF@pRX4BH4B;ic$wm{%)o&xEGjQhO;?4AOS)7oBUqc5;tj z%Q-DaKDYV)v)@nUZH!pn-q6*aLGiJbnZgOn(zt~9qL@@qHWBOCCZ3_OdMqjSFdW}^ ztKjLHz2nhW&TL412f%@fH;CiRkUlCMs(fg(cR!NioG{Iw!Vj?`5WGmQT(L&t@Gqw> zaa^45nb#I1bR|9k+=`&a{ZWIwMBmvG)yduFToaq(L%JenCdg`uCb_a7A(@o|yDO<@k9e+`7 zn^1%qTxzwnl}%nji+1OEt}&~m5A(ZzNQgJJ)cx{X+!nW?!uXcXHY)j)yXB!#+&w~zz3PThHV-`Yz2KUnE|WABrz@t zy5N~wf6o0|*VIUYL)q>3Yt4VLOK^rZuL=M40_R=LkgaGx+E6bV8u|?w3B;;`QHx%e zGhiV96_bDbM!agtf{DxjMJ|D&E9H&%AxL|mou14BuEozXwj$NLs ztl2?kcPZ~ENx2=D3(?_H2mGN!ziz`;_}LY2F+)})l1twNFY|GXQ2F^Y_`MN|<~L$! z58FpZAz|_70AYz--o7Te9O=P9dDCIa0LO*37m`x$y>-W-F%>Z5gIC~ghP;63?_y?} znQ1F5$_Iq|jp;gy0CCOmhXtQN3tr@S;o+stvmIVF17j%f(kjeQdv}kQ7W|CZhnn7? z;=%%-46qw*gs55>>p@LVAROy-u2xZxc>{PO35LB!#S|IgwHGb+P%n8wnjR`@Cm?F?sJR;)JFK1)26SL1zFj4$-Dh27U&lG6W-Zi_pIpKCHY>J+VLo)tF$)zlPcS3gq7 zujqB6`#^8qp9kIORn8#6;2X)&yLkvjZ|v^XpM;)tOQs~5Ub^Ujy@nR<|8iU5_fMTd zp;PIJ1IPbEF^B;IPp!tISLO@DSaXQNGs=oA+w1#N@dW`^zpioeJg69}rWT|Dw&$Hm ziY;oQ_dTty-3O6Zc>5zXldEF*EO#J4wo*O#9F@!vwxZh%#*Mwxse#-r`08W-nK(Ve z@2+LS7V?Y`lV)CNKxfi>^b8*_cbR!XyDq@pUKgDCXuc+$&_OgPbviX|uFUGUQr=tY zzIOqc{-$Av;ljiv==}va z$lHId4ZnX)sVQ~+!s%kv0Lfp)8UhgA{Jayft_TXO!IJ-GAaMK#;8d<1J(YZD$Sd+* z!@6Wk_N?EZUyFgvseL!nV6Kk|6tW7A?wYy2fZoRsBt3 zu|B(p{cK{^P(>!BqHNpsfV-cwa;Otpar+)ipw%tZ$s|O}2fiO+sm4aIA$|X@n=@~r zx*kXeo(ST&5H(07v}(i`U@9P6rOmcafrtMwDf}nV(*N8GEbK&0(I;|uZ()otJ!pLG zYo^*z6l5#^v&JydSP%0e-U6}s|AZ*4Y_6`9)J^Lr|?!OZ%le0zRpE8~zq-qRiHo1B5T+45i)AZ#QGZ0XR zZPmlJH?4kJy6Ljy>nRpv(cN{}R2xn`jxSn$QraTqRTAfSbxq;*ji9)`-bNE{7e4Hw zes@J|TFN!cqSy=(Ije1EgeS3*WOhhP3BBKonA<2*qxWhgU#+w)H*yT!Tfc{lC~@1` z$zA3IV4huQ!p1eO5!xhh!tAm&mtwQk;GL_JHCVk@6Rx&8Ht9gEH}Zb|Nv~a%iC)n2 zxgJa6kiBu&q#oRN9y?ftHBl!|8=qgjaK$0F^6RLz`%^7i@bZ-*7@iYz!Z9{LS`VcL zuCqE@EkEnd(j%8|cFuLj-m^bM{)gF<5Xat;$B1rxM|L3;AA$V zMf>x+PpFfz*~K4mw`juWwQ!a>FKk3}*~-!2Yzph$MeMBkA1);(VBZY4ZZ?XRRyNWx z*jc;=*+chGKS^&teODZ^>+YrscUqRzLPjrF%B|}3HR0vAncw=265RsLjPgt+GgSWr z_`xMTcmu7Qs^D{x2#Q$ZMVveKH8|C_eIm`tr1W5-hWlKWn!BZ-nv@wm3>-1jI~Ets zbGEA;2&sRcV%2>At6?XbE5|h9GvB?{`@#O;spI~~b@j316Wi$y_>i_S6Pvq}A(>hA z?&$s5)^RCgeEVNxW_^`qnTZrAO~t&->A0olX5YG`I8%zIFY5l2zAB%F8njqGqqs|VXIX@+QzwfI_^;>GT z!>yKUqe*o~r!>f-xOQRH7kQ_o+(D|`N}b$+2!v8htroi2!+pl?av;G=2iTjC~yD}AbwYRkwc1D_6E`X_Dzx|OvCBCS|$#7qx zbF$nZgrk>cCDVjw3w!Y`Z7d{;b8oH6XjGLP3&TPId!#zOKTWo&Jf87gdN1q?-u&;f zLZ{*Brr1V!_xo%)9?-?D*&{6iR=g=WGCih3&WgNzIO8j)>4EP~DPzhi0z+8D zl$E%{Fq>D7%Y_L37+#e+OG1O-IGVuO$g@$blGGUOhcl!LlP#4|?+49A`1e)w)GU`li_ zl#{bnSEIXLar&M?_&BiccA@MY<)j)tXezPD_V^P0WBV4tXHZ5p3B?(6`^osnP>!B# zXJ4f%eYf*vYnx&E>Z9I0y3v17<@Fxw{`YCUe@D%&XB_{U5&XYAHH;7Rn)eQ_5qKo~;V zpt_~2;=E9~n0I!JzZ4@*8`%e?VpX&1+gsE1+#c+qbG(k`9aOGX!*-OCwg_2v%RQX= zlOwbc)s5cWtfr$sYa{x2#<{E?{dV^pT-0amCO60;5o(w;OKhRwX&DTc8=+6Eep z5S1}#@8c$~axJm_Oo>KT1pH^oTyA-~-xlRljQ5;A+GS)m8bWM41@2)qFiFP zbg%O7Sz>!+%iXW^2ro(`n;wr+A21p!^y2!NH;L*k_}Mp$+Iq3zb@fx4@Ha;Vn&eU8 z7+CMRti83ZDZ**=OeuZk-parhFl0Df-N+xkvT4tRHh7X`|DPnR|1YyAp!dJYun*f% z@;s9>jn0^5nME(Jorr9-rI4+WAzy?Lb7{cvpEp+188!{iv4iY+i`z>+aHXCtMJz5o zdti?r&I=@aaK~DV54zRU3nxJ3;4uOW*EcJ1Hk)d{H)Ta~pRirLGV$5w#GKJVhq093 zr!JGSP?Pk&Vwh}AJbe_9rv18AP4aTUx$5~nhptCeGsm)RKaQ**dgt2Ef}9_$wN^!p zkP^YIm_y@!P~@NS?NxKP#es0q_o%)GSxW+r^E^@AsD5j$>{j1oYt@)$PL~>q6aeP@ z3i#-BTosHE9&$=DOOkfQ#^SlDIN7H-&q!kE(GC=oy4j?m#m4@aQ&b0PE56IRn7DC4 zp+=t$_g`#11tZpRwSaxF)`W+d1w}8vdEdI3Rx~=mn9zhAjcgPr9(OUj3f-t#{XFFgAnOZgV!jb7N^WR7|0bsr z+0>TD@e(#rV!On9D-q_vk97w+vCI~r$)afj_LS!8AdKk+*5 zS!-K?ZDG^Wqu6(G_|xI<^|XQ4HN0$qeXh?j|7>o_q}~$F$aQk+-qovDbJ0@Y*bhO; zlaw1w@-|t@(1VJ5>^^pUN;zT6_+ratgt5&EbY%iHHJ$Y5pIt+RJ_pH&6Zu)&+f^LZX5KYLMNGoSAFKpE$p zN5rNi=$vA%ST;SQB7k2D)5YF35BG07iQ95au=_7jx<7|HWwRo>GXm)EU->e>wGx$$ zt_W8ABSneT1bmcy=P`NX+_Fi`ib;zE-Aizvx3i`Ma%(oS`BJgKs5Hi~M`jeE`w5ML ztc!ggu-EC$z$hg3@qsSJqmq#ihv<-=5?j~hb;JXUSyOPh)r{qYVPj4}E| z5LT_8oy`=W<|2So@mzl)l4dXa3V0>>;BkGylGQN!To?ceUKLRSfwYBYr)RiaFIxBB4lO@*R2K%zdq*}q!!Z2I&AM{6a+9zghMN90a z+SKM%fo{`*5ux2IN>tbq3Y}`YJqihXEAm${BRruiUtOsH8U%lybK&_wYj2Z<>!|HAJ0ipY8(Zht ztp{JVc|Jd1XV=Zqx*GC+Xx2QGhcjWnV$v~k?mH!BP7B^ue;c10wMM8S9?lJ)Y0L^o zvu~fDjqLO#>+P&CZXur{78BqBaMynCcN+bAbRda&IS-LgvxezVuDL1k11{J-5(B?PBBH%Lqmrq#f6lLA z(FL#L6=3HZVt{6rJkMU<)BWno=1kJ8$bZJ@fQ)@w= zHrBs8*kZ-@3n0ayvcefF)4tX+W)V)jbq+UaY9LnMEPj-;%h#a zak27jNA6=M~ok-YCCd)BU7K?{zebvS0)W>jZ3KQd~rZb80Z3YYDiX|*)K zsnfqPvT^iqc-1EfHWND4y_rgl-CpW|4-0`DrQh3H+vdara%tN{_?Q%lvrsf~|4eF?fijU_0H)FSA*g7+<6p-Ose4`8jgKl$U-V zoW>zX>J0DSfkZq^sE2)pn=g>A5$*viqXlY^Is18BFzUgjtsOHB9nBAIo) zsto50&e@{ska~tmz^>|z@O$IYy%-}W58?(0c>uJfk}J-m5H49w-nh+;E{%@f7X6oC z;1a($f_PAUwJ09F7;ca5d~tuf9j0&-EHIMI*Mv87(+#oKaPI8g^ic@lpb1ZrPVh#| z))FpF&eX;X7e~_X>RB2blSb)b3)9j^{qY&cf~{t&X`?btvQ!#Y7B#%hFV7()5%TM< z?*Rtn7g$WKVe|uqFw>>Xnbd`r2HA*$qT7$-%bc4@hc6#a2f?+-Q9@>~v{ud7>A-d& zq~N__d3xA^-yIfa_Y3y(EK!Zd?gsFlu|I1cn7Q)K(5Y4*n_+EW`g7ez`ZvwK#3RMj zZsHH6PSeuayy@DR)^q}OZsM{A`JooQK_<5*jWjrdB_+A>Nqg49#R7^vNSv;`DhV%Q zXxsA>(c-1h^t63GI`E^XXvJdnd;M2eHs1W`AxIo6BRF0^qu*86`4Y^=S~})=CrZCL zH>w{##CI_6=3(2oIYz>@aET__l>+&q(Ru%a-t5=>-00Eb(YQrd!v;|!;EmP_P57mo zmGKjc(9>fbaKVX**<+EA+XhoNdZMXi)5Zr*b*mE?r?)NSupm+il2i0HqDE92|_DmU5n&^_?dGT5woX(iD!iu?HPvrGTF=4gB~GQ zRyarVDxBtja`&VVo;G~7GFn%{Ub#m-;TTuC8k-(U^~Os#=bbewVw&M=8lK(2vXjm< zP5J1Qy07(>GBi4sYdkaj1L;!cb0Ww?4<`&QtWNt$hHs@Wqm?Jl$crQ;yihqyd>I_z zuo>7#?KW&yxT)s;r&{pl+mEDI#bMbfUF;M2)y3Oo!Zmh@bWvH~64a+sB#+!+)GK=j zMw4kpz?<%!E?poyoh>smlM7eiezB+L6ox?y)%M61C`X0_Qt{>%2o6)#-1iC25kY>z zXpFx+P}*s#LH3+D@`W&+to20*)32p$5k4`W#UDCRWGRX}-Yh-UJW<}4e;PkLZTH6+ zi{8#pwctt-lgEk^%Fc+HikH%brmc+p%q@)71oMR)&!=uy|B*jC*gx62ST3mFY!7m8 z;)(qeM=bBY;Dhv=_}-z8%2?8uq^H|LpU?F(%MWKV!ujE*N_-?GnU-pNTq3(gFU2>h zX~BtOQ(~g>Ew!vfs0_eoPu+K@>x2|yYMUG3m9DlapY@WTp)~XvDKtv)$aGIdj8$ez za9<>5E!B4E9g2ihsQBfxrB;kzt|@6m?iWiB^pd1Jl*+t)sj;KY%pEO$Gh%S~bs$+^ zHXqLo^+YJ58z;I2YVMMj`-(vaIc4JdJ}c37^kA7rCVA2+SLtSzNwv3l9zk~gcG#vl zZhTc>DOzi$@1fQyJCubCxu7BFqCo*6Bd3l5uOFG}7HN zBO)=wR6$iyL zFo8D286A3X`H6xOdYX&IFO2h5Q|Iq!!^78H$Y@+1HXAs5aR{WhlZQZhUX-KXg@0q{PD_kY3^;bFdqF)nt8|F z9@ux|Vuze(RnkVpi|vw`wdkwaUz^~KiYrm-EQ9C(o+epD&r?d2jC1u%Nia_aQc*N= zp(yw(P5s;xmuw%;?h{Rdl+!Xx8$N=n>!IBRZVt*#u=+x_8ns6>0-0Xy_;hn+`#7jI#Dt4W>OF=0%^;rrde`wqHEb&v9^;!Rpe zYMSu-<_l}2Dc?5X=xVmI5$Egexmfv-fxTVplzrKj@CL*2(sGzvJZj{iZ1NFf{*=#L zngdJ{0t0FXAkq#1+(mx-;lcPKo5bCWeAkhyn)h_EJ;XzSj^zFMZcTBkcSFVM*|r<3 zn05JX_M+V{xxeKYR)3y%6gNA0H@7ogxcHr#`+GB|Mey6(VM6%BO=dzZ+uReV zI8H+|?A_~>V>75w@uqSyQFa%k4$QX#M!0scO-Wdwm%x-ybxM>2Y?GGNt73g*pdvf4 zqggOkmOFgQ(xV=Kl^67Dgl#d6B)0urXk#tfuhzA~bZnR}l3?W&AnubfkwT{7!yyWj zsgv|jV7ou+9ME^HE|tFfy=j=Q*o7Pgm06ARN zo_RBgkP33B1A~t9^DI;ZCC>nB1n0q*W8ZphGpJH-tIl`ty}HKJf*+j^$DjTbfcriI zM+fqj|6F4yGC}6{Iv!l;zWu|R6bEqLGIP-{;%*1wi^>DEJxv1em&d#QH8dY&kp4X& zAb>9|8j}?4-|0lfqN>*AvTddlskkPd9jx;A9dw^pnYZiVY`GwM;uXel9YCnRrF*hL zdz~n)ze^pS>r8?X&Nj=JSqz`hW);rv&Y!l75|bojcIrkIJJ!PROYfW+G#GKWs%Z0{ zf7^Yl0k&RAj#zmv6M>8X^Wr~-1^&B*F1qhRF0<5KE=HCsuJ)p-{h*$+jsv>Sf{V`i z?Jjxg#e(XJ>y<&w>wka@Y)_M15Wl2vC&@a6)|nDU-7ZTA0#th8;mp{fNUM6^XQQ^s zBpg5kDPmPy^S>LQr7c z=AubY?_q zWKK$_k7d6d)aRoj5Ppp25NzUG(S+xEovz3C4ZxZK3uMl#R{L>HYDw{gy`a>Zv%uOH zv-mLbY14V@Ii^_8Ngi(Epk3ar&LiN(LmdmXW6L9Pr;kE>5wR5l^??$$p>LFK(1YMm z7)-gy*h=k<8wpo~z4O*`>JoR{v*CaAD4IQ~2rmfeUU8wnFLurqfAz&Rbrle5W-q{G zZM3li@Q|?-9b0FB0Gm1A>%cF>u%GExx9rx0&*|BJpcoHP9CDQt(4IR(I%_zuNv`DA z8Dj4cH|??!O|~1XL$yAvXdw!+5`0XP8^QT!y>P zboe@YwcshZO%>Mc+tp3$_1@EeR-^m=2ZQ=Sn6oU>@fz5(q2PiK7}XB|v;Pj@`p-ET zP}Z4zsK(ZzcrSU1k_pwKXIdbH1g~Od~veqbhVJx&VB3_KAJxaG?_)JDO7yTj{Qi8`=-Fbv(Jt~x)r6NrX>9(RsZNJAqg*U|3T0}CQx)I^NKo6q%Wbuc znm($Fb&G{{@L;8iM)@s|WsAe!e+B3)qr4MHS8iHfkJ7yb9l1+1gnt-rjxQoohcCO{ ztBP;;aVlD&pv6a>vwu=obN4q_sm_sA2#w>QL7vV(-Q0OGU5zd>K07~<59`R%C92=F z43VPT9Hl{#TR>7Bq~`-_j87`V*I%#$yx><|?D(T=weJ~e`&e4=xs{$#;tJ);!@9XG z&g5qkiH)>bgXmL#gVxg1KDaI~jrVg9RMKy4*=JH!;cWcW9sDt@0{GzTj>kT zKoU9UO!CWx$kaVZmSkVuVBH;>3J&t}!`^}Hj6JZ&8Ap%c1yAgKb|W)Q8~7D0aT@W}d<;aW%SA0MHF~EM`K_#(FB}D8A-|{pz;xM*M92uT+*0-)Knq3S* zzJMfn=a%;%P&>{URp``p`XWg?`Lbo&FH7} zGiFFO^ZeNF8kZ|GYuY^4Fb-WQ>(I9|VBhtS!VMk&1an*aPuW0AHHxqF8sd130I?^T z4eNLFHaKYC=ByjQyT3ioP=kD_zy-0~2MfEHYl+ODS6ZfAYQLj6UUfzs?va1GH}=I^EP}ZI_cmho;k~C;1*ups2u|NoJ{>c9tXQNp0 zWw|1F!u(02)1srmPIRM@?r2#(i!2=xyZ!e^C!!(9t*bHV_7$D&kO11YPK zItc!D=|krQ`xQ-!4!SWv4N%NcUb&Y;PUVR$XD4g?t8dY?>)ZuO(St^BLn<*vbe7L| zaua4Y2n)x(%rE?YC6Vka$R>C77+%Pr2ZVe0?ne&*VAi0+(VaO~Unm@gD;y6ij@?}Y zxNwT2zc5R^@YyE~W1sYD?!55HMzvQ9)HYOE zC{x>QN-Kfwa%^9+DB>gNd;^s)B>4VsL^JKnzY|Ste|O1>40EUQ z3cd0omU;>6(jDf-t}ybor#he~kKLW&0yN$8%gu=V(aJUpi6h@+G@4#TgpL>TY3|>O z(T2-WwKxAxDjBq@q0Z&C`ghON$!}=YQAXGyq;#0Fh-Z-4es!H@0cmRP3t0^6`p#MH>enQ7=BH_mtz7BkBd6hO2!wE<#?f%5_ zjC?=_+72|y3Udbe(64%BsvT889?Rz-#6HuV5jx;dlm8|PJbZpfrlb6_e5rP1{FNnk z__*Y5?nKDd$&`Du=WmxA9hRauFi^+#H32kCn=BYJJAF5S-+Ld;TWLc@!*GqZq6k6W zYL%r5P1xxCK}Xvk{}22>MkQ!uyG!dr`}B^=Bqr@tZYn9zhO7Wopj*ynI9u%Tfc%e3e19>Vy3>uWaCSTUW>e~U$Yy9a`jl@1N(18 z-sf7H2)Q(cCJT9T4(ZH#cn8sTGtH3D4iNmM!;yf1#!N_dN44SZ;GD+0OFD-mZO$5~ z|4GX%{P=)4)!*UzcEhNM#*n$}g><=sQ2|Nv%3_nNn!7!mG15X+J2fY^Y`V;}kCI{b zUsK*8Qb6prp9WYkRtaY2%A^>a<~GcG__30&SZFDVrDNWiQ>^PxjvfD2m5$L-oXq$v4-SfLa(-YId*okEO&jMYZEsn6;a>T zDFgA3FgXHRsk$4J@>HPSj zE75u=Z)VbZ;wHB_u51atr#Z9<4$qvF@eO2+M8xu%URp4AHqa0!kA5I;cr_YQ#Dw6a z(I0^0&sRP_OvZW{TpF^u-)VDDC!L=~*}9c)gSnvVjb!r&7hKQV^CHrkUHLYs1pYX! z_Kr=4JUqX-1%Gg)p+%`)sfd-E)DRLH2*Xl7R;JKronaA>n`r`SrSETX$Wvlu!isn= zCEC~V#w>w4(}U;~;X_s(#oN-%yYhUomZNKfH~5~Yo(1c<4ONZEwLx715ooC3Njpi} zm#|%W>OI`bKzTeGAX5T~8AIHD**&D(ppJbCFO$-_+lUAc5-XI25Ej!~1eKW&iKZsb zIij;Nc?#&Pm#JR8J)qW^D&{KbQ^-)W~Ou^a&IX+sDeEi!i)l&>lk^$$XO`Gy@s#&NkZh?Og3%AMBtNpxnz4e*&VpRc3t^QKeODWvdwYixQ$ugvEa=6jKCMe8 zjVQfXPr_!G=+{IT%R$j9<;O>t^;qYSTxorNnDt_>+Rh z+u`TeoW{Dw1fd)19G1y|11X+z14)c=+W3tuE0a9V<8r z>E$nhpM-z&Z5o3A5qe?5$LBZPsgeB)iPyx_!B@ZggehhZn`B0geqy6#)=By}dq^;V zYl$}m9b=WU&~^#W9xdu)yGMV#F?DUwZGT*E?plLzzep2?lWO4wPHoT5H%ig|ECf^0 zYPl-8@K#it%e>IrikYLra0<;(AY@PYYx4I>&AoiQS>#j2AjAq4ko7@9=%I6a*xSi_ z*hjsL{s6$G`Xti0Y!#>6cwoh{9X(r$?d)nlIi zH9;v}baT#)z2PEY#k?s-nNeVCIX4?a*JuDwR@WUV&#U@r=<5q3dx<7(!qUa6tR{~U zS&gqmNFyWKDz!+>+{#6@(N~ow3S|-m37;WAf``g^hLM%9XSGI;1sjAFG)BxeAZ}7^ zM!x=$m64LDYE+HLgK*|@18m02s-01e2c1hSMOQM%_3R}A?jfM1P#+9Or+R2l=u~U3 z?1~FDuqD8NaLIJ;I;`0K>SbirThM5#4&(D8Ze5rL4)+dXqRzEh(L2kwN^ph%xDF|G zRsXFE6vqB*KyG?)sqE9gxPv^yus@qeEQt{xy(lkrf{baz5@dHk-qohNyfJ<$RR7X z-39b6-oFJ9lZ-%9#(2;>kesMxI)a!mBQv+D)@a*av)H&Tvawo&AKVAI zh3ySaeoUNShwdG@+$Mp>*Rf*Nj8w|h`Z6xJ7y0Jpfm_%f04ktRPtiHClM|!g5bIIb znfudb=Ny5Y6^{DzOOaNskD~v*7P**nZW}cbI>X-J|9j$ z3O#kMomEIB70Dg#XXF}akwFY+Cg&Ll(3a>Nm%W|2mo1xS!_Xp4Gl#xb%Y8ec$#-g@ z3kLm5P9cP6*FtBHB%|N&XVMOEFX5xymHg=-viOrPoCFO0n^G~U62xMr+Illk%%|BM zG^6!xmve6aglou~!BEbiU?9mcp-5>kfe^OPF;GIR00(tV{RoO10_uaBGROQvy&x(2 zeF1E&gzCo@{@F3XG-^=pS-TH)QZjGaURaH7?^;+cjg^2<^Lz11Wg}6!JJbJG00ow| z2Q*mUSM9yZDMT@_o?01#8dX5&nEzn=N9%z(ADjiiGT&Km>Nsr+e%Hm`34z3Jz>^xN zcrvk^e`d9I?Mk-l0zifRUzDc*)H+Yo#qKo&Xu(+!R%KAv+rwm#4+}skoxIuInwG9Q z5+(EDhwu@KqW_E#?VspABy$h5K?>~_KJ?ZAMREKG&^8)7cgg&frWrqXtZG{Vk9Wef zYrQ2HTJxHkyJI)#jhdMX&3So$dNx%QDNIqN0T=jCaz#ebF#OQJcN$_;Uk$SDctkt- z?U~5=$A)oInD9fAvkx*J_-@cVSMg;??=E1d2I1?ccqb8}5TF3o4B-iuSfFkozSy1$ zO#mQsgMg@2&zdY!U=4bM73%GIPE6>kZt~PrkxbrsPBpR%YSg);L4JGnZUB#DH}}b} zeTq9%0w{omXMAX{0V6=ubLE)XF;zy&MFtT&1DfNu?p4KY1Fe@ZTiA{_U3Ff7YtP)y39l=pfe26=663sA?76{@bo5rM9pQfLlP- z=HLBp!+)vt+{@pJd^8H`n~z#Xmu9=B7s}%v#@0&k0Jn0T^{VyM>ul=dZ6~5&CtG|S zm3=Sp z>X`7%r5QEPy=dJm?8O}eb2$C`LVJRE_!$Y5w- z<#VUPGjSX}!uC=p<0~{(73%JnYV>EWInR1E%|K!tWNGJ|pOTyPTDnL2TR~xVLo|q& zISXwawbX>7C{P$R9k!O41*jm@oCn`v~$9&21BU1?Ub5I*t&G@)L4J5OfAU~L9i7<6oc z8;}#-Z#3Z>p~_opE@+R)cQ6-KPju^8$(KTj1Lt}-(}z3q%G1-VPY8GCMI0Lp;OIHH z2^wBh7BtTu62E^amVaMFVmZ5LkjDlrv2OGAGnGRJ08S4VBWbw2H?+^#Yh)$?qgvh& zT7KI2^qg~LlzxCz`Pu^$zL6~-;ngVP&d9?TFP9<&YXb;nIZrOM@m$tCoMR!Me;A$d zx*v1^g&$75haL7Gb|D8g?ZvURpr)5HN@!YhZ1!}mK>0OV!RH8(%* zB3@K(*R(}=%O|PIX2z?k&idZ8P5i3!?R|CpyqYIQ$gJC_iPkDsczXzSpS^alE_Pod zvq+6z$c4w1DK>lzj${q;gOp8*MFy!XF$Yw;L&O5N3Ae{{t*1!3GtR$y%(IbI;x_He2kquZHos*9a%H#PaxUl|$iySiGQKPlW;jsNaJJR&S$O;ifz#;oghb zrGdCYdXySH3a!bY#rDaroc7;87|q$p#t2tab>P|LMN#EKz6!k$G~#2ytE%4m-beJ5 znKXE~=txqs?Z*%E4@IvGgmAou!g6+wn!t;eqU2vcRM;ywl}qpPtB6^wLN#}(yq1({ z2yjwxu0X1^6`1A=zzQ?KhCY$kUX7u44#(W~(&T({gLZAoF z_Je2+0l0PW&;RSkX8w!P0?KK_-M{-z&B0B=rbRdLbap83)lF4#Tt)-l!-XKuimDba zQ582n;GV(|;KHB34YT~4pNu7q%GaJHJdN&>tMk3tpMr`$c=dTdV2E!UVx3lE#mG_c zf6pXY6d$(icPS@-n%a;t%x{^i@767{LGf2;q%`&3ERFMT_{gtm=bslUcwZSAkK6;ftMZ~ zqiTO;CpZwi8i%3aLSDGYs+5mP6ur1J;yT5gbRRf}X#l(01TYp|^&s~;qD~$?avEO~ zTi;~?>LY}j)g%4UiqJFiRpL3MHBY5!P8X4o`?m%OUrzL1o#zBBo{0gda}QFcB0A2< z%&{a&scjwOooj~7hJfhcq|>0{9)SE`8g2mLpn>Ca=3J#`rn@$r(tdmAsHvm=&f$vY zI4^EY`-ByM7JQV}A zE9@y*)VMHdM~TY4sxk{x;P@_HQM&s4VRMCQzN_>y>U`UkJEnN$5b6J-m z=zaSIQ^Y0Bq;&Dzcx0zCtvuwE&f(I|qV_z|K&Q;{PX}FNS<@*G8hd%~7Nz6oV>xz| z?sS@fVAjm7DZ{m&l;g`QkdDGp{^v-_5@=z$ehn~&g_CG)jz?3vMGp_+IWwa+eF$8U zGSc8UXmXs~oh|0{qz@M@vWuq|JWUVZ?Or@`Q&yPi4rhaoGpeLvN>aPFOYBLwU!v%t zGhiKmGLka^0_?R5z12k{y}z$@bAbezx-%as*^hETU-@amZ69x`g$$f{lohQak1LAl zs|zLhAgKhS8D@usWoNQs!*>Av`}1A<1TNcgRfkbTtao@jYYh-tq9y0sB~A_|hTnN4 zbY&#C*o$7wo5qmm@Z-UtmqH|u3s^ndz)yIF3E3~1>yM*srrTIqi`MSt6_+TN339PB z@$?zxVw;rOc9~eQ+Ux*2LIktF3iK=;0H!Hr2LEOk=FM-PJ*75sx;5Gr<{r@8fsuE(diPp{Ajp>o<g|tld*>?CQBix{Tj&7acb~fQdx=7^ zAjB&ds?(m;_uR^qsONM)0$eye3hHl%3zsVEq__H|RQxdjBeLBBUOt(asFY9UodHNa z*lA@Y)irLB!Lw=UU$bG}!Hu+eIW%lSmxamt`UZE-gqRIy?+_edJ z;k*P&5K&pkgoOI}%-vuI?3RdtLajc|_dcWb2$619fj6$Mxk z#OmaSEA>t#psUdUbTNQ}^g34cAM0!tjP)PqCqT;IIqv1^WVTYy zrY<8opnlHQ`J1k$K@RJ%se7tE!3}SQuX0wWZK!&PQq_>A8_*EwlX8$5-LUw%b*`-l zPE@QnH<};3(7Tbp6;jj;QIuo(lsIXCprK6w{F%Y8hz+ph_`NojoUEiAUDvdAz_6(ij_-4c-= m5S