From 66836ae54980f8d1d51cbe23320e2f6a98e996a0 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 26 Sep 2024 20:23:45 +0200 Subject: [PATCH 1/4] Fix homepage and add Zulip channel --- home_page/_layouts/default.html | 3 ++- home_page/index.md | 10 +++++----- lakefile.toml | 2 +- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/home_page/_layouts/default.html b/home_page/_layouts/default.html index 22a44e98..a66082d1 100644 --- a/home_page/_layouts/default.html +++ b/home_page/_layouts/default.html @@ -28,6 +28,7 @@

{{ page.title | default: site.title | default: site.git

{{ page.description | default: site.description | default: site.github.project_tagline }}

Blueprint (web) + Blueprint (pdf) Documentation {% if site.github.is_project_page %} GitHub @@ -46,4 +47,4 @@

{{ page.description | default: site.description | de - \ No newline at end of file + diff --git a/home_page/index.md b/home_page/index.md index 6ffef044..e4ffb643 100644 --- a/home_page/index.md +++ b/home_page/index.md @@ -8,8 +8,8 @@ usemathjax: true Useful links: -* [Zulip chat for Lean](https://leanprover.zulipchat.com/) for coordination -* [Blueprint](blueprint/) -* [Blueprint as pdf](blueprint.pdf) -* [Dependency graph](blueprint/dep_graph_document.html) -* [Doc pages for this repository](docs/) \ No newline at end of file +* [Zulip chat for Lean](https://leanprover.zulipchat.com/#narrow/stream/458659-Equational) for coordination +* [Blueprint]({{ site.url }}/blueprint/) +* [Blueprint as pdf]({{ site.url }}/blueprint.pdf) +* [Dependency graph]({{ site.url }}/blueprint/dep_graph_document.html) +* [Doc pages for this repository]({{ site.url }}/docs/) diff --git a/lakefile.toml b/lakefile.toml index 9b525148..c1a2ab13 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -10,7 +10,6 @@ relaxedAutoImplicit = false name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" - [[require]] name = "checkdecls" git = "https://github.com/PatrickMassot/checkdecls.git" @@ -19,6 +18,7 @@ git = "https://github.com/PatrickMassot/checkdecls.git" name = "«doc-gen4»" git = "https://github.com/leanprover/doc-gen4" rev = "main" + [[lean_lib]] name = "equational_theories" From 535c74e25a637bdd932b4f028ee26983678a9cc4 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 26 Sep 2024 20:24:23 +0200 Subject: [PATCH 2/4] Fix a typo in blueprint and fix CONTRIBUTING --- CONTRIBUTING.md | 8 +------- blueprint/src/chapter/intro.tex | 2 +- 2 files changed, 2 insertions(+), 8 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 51c22550..05efdd38 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,7 +1 @@ -# Contributing to [Project] - -Thank you for your interest in contributing to [Project]! We welcome contributions from the -community and appreciate your efforts to improve the project. Please follow the guidelines below -to ensure a smooth contribution process. - -... \ No newline at end of file +# Contributing to Equational Theories diff --git a/blueprint/src/chapter/intro.tex b/blueprint/src/chapter/intro.tex index 801b1617..ee6eb746 100644 --- a/blueprint/src/chapter/intro.tex +++ b/blueprint/src/chapter/intro.tex @@ -3,7 +3,7 @@ \chapter{Introduction} \begin{definition}\label{magma-def}\lean{Magma}\leanok A Magma is a set $G$ equipped with a binary operation $\circ: G \times G \to G$. \end{definition} -A \emph{law} is a equation involving a finite number of indeterminate variables and the operation $\circ$. A magma $G$ then obeys that law if the equation holds for all possible choices of indeterminate variables in $G$. For instance, the commutative law +A \emph{law} is an equation involving a finite number of indeterminate variables and the operation $\circ$. A magma $G$ then obeys that law if the equation holds for all possible choices of indeterminate variables in $G$. For instance, the commutative law $$ x \circ y = y \circ x$$ holds in a magma $G$ if and only if that magma is abelian. From baecd83ddc520f7d26576190a5af3c747ae4a746 Mon Sep 17 00:00:00 2001 From: Terence Tao Date: Thu, 26 Sep 2024 11:56:07 -0700 Subject: [PATCH 3/4] added updated image of graph --- README.md | 2 + images/implications.png | Bin 0 -> 36962 bytes images/implications.svg | 3854 +++++++++++++++++++++++++++++++++++++++ 3 files changed, 3856 insertions(+) create mode 100644 images/implications.png create mode 100644 images/implications.svg diff --git a/README.md b/README.md index 02f61e7e..5b00ae2d 100644 --- a/README.md +++ b/README.md @@ -4,6 +4,8 @@ The purpose of this project is to explore the space of equational theories of magmas, ordered by implication. To begin with we shall focus only on theories of a single equation, which are listed [here](https://github.com/teorth/equational_theories/blob/main/scripts/equations.txt). +A (manually created) graph of the dependencies obtained so far can be found [here](images/implications.png), current as of Sep 26 2024. + Links: - [Main web page](https://teorth.github.io/equational_theories/) diff --git a/images/implications.png b/images/implications.png new file mode 100644 index 0000000000000000000000000000000000000000..11ebf37d1312257efb16e4a63c3cfd758bda8248 GIT binary patch literal 36962 zcmZs@cT|&08$B98KvaqXqS7p(O4HE0B1%Ad?{JU+(xrDeiYQVf)DQ&42uhdGYXmhC zLYER+Km-iENekr;=lk7z*ShQe;bN^M@65b2&pc)C{rJ*A?*a3fD`y}O2s2#ko)H8> zs|kV7ES_cnpL~g?w1GcNK3bN35C}{A$v+yr_s2)z!^{4f7XHTG2>&3*C(e+dpdbl1 zFLysDM;~Vi?)Ff^-B|t za->Ic9lr(V_kw?a4im~#^7BF}?GX3UQc%-5eq~BpiuAj=sKcOVvSGB$FlyIt%{iN$ zS4Av1h57M6T8ig)bzs+!($@W|NC|gO7laxkOZrxt=r8{=>ky;gIexb4M*KbwTEW@d zh04kNBhw=GwB4v@y*X&v(Bl8b_{c+dP#5qNWh>yete4oe6bVOb6`?F6jIR5ab%uQS zp)fzHHEPj+9yuvSQHSGo_H8~6B@Ex%e!X=DE>!J7{c~Dh;nMExB~~nC#MAkgpO@f< zc8XuOxOXlp!V*cdN;^mMAn>s;B^Ebue`Gis6;ZjYaH~RM4dTP*^9ds!{pS8i&v#t& z`zR*1QE!F=kAxmSulpMqFt3$XeDrE;TqBKnHi>NwskhvRCG~%ky z%;_Gu$I?J7Kcg(KyH9tQNiK)NyvL{_;RdJ1eRb1$er6(^@wiAH~ z0?2y`2KxyWAyHGX8%r*(((APpx{GCBH*?S_$|6s?>n|c@PX*GK(FM}X#d*Iu6^?B; z=7VG;RCIoq8XIOeWMNdd zPQO5igk8sO4%+wkO)I7O@k(eH%|*23`GO|3{!fb@oXMXBeAH%l^UY~lvq_pas>p1? z#i%z5gu~(Jvt3I+eNPY9U;a|~TWQ{g8)iN7@L%H6yLG)6|4Kr*X+&mAu;pb}3#id} zXeo?v*m}Co!IakDt6=?PufMA!f5}h6;K;L3l>pAbzkySzG;Ft>D`HPL*H6{we%3WP zqXaZvEb7pU6P)q)^%dBB4tK1yZY@nxYE_gWN0bz{laZ0p+xDf~Mlsa?)i;FfQps(& zJDQ}CdMU$i;9nulZUwo7mX;P>;!;+=a1zo#57UViYy3`RC{F59kUI+BM)`GD|5;rn zR|v;*acHjFz?0z(b$zZpvV@gV!_=zKO|PBq`cGeOYIfIO*6+{u<>42hXuTaKwv4$- zmq}qY+5MYHaAY`luu1=Lr5Ls26!TnQcVY~fx&AWT$UeJZlenabsL|ulB==Mqi9qU&Y z#Y5lzs>`38oNNva4Yi~7Fy;96E%E*g@@0{U!o1=p*iX4q8Fm&pUemDZJ!;}Ah5K*l z;YyLy;=TR_U!FX5g@NVI!toMC!;5NfmMp!xyY8J#Rqz1{52Vq{s8aG_U#k}DJTmdM za6%SP%y1&eZCPyIeZ#Hvn3$L-Gu}+Uf%KD?a&syw5s;pQ{{8v5nl3(Hp4p;{DB&)B zB@<0jAN;H!_a+#4fW^lV5fNw(P2cN296mu7I)CC2vL*o@?2g+@q(x>HmRtzW*>Ovb zZ}XeV$DV_}3Ua*vJ*D_&=mMc~$qMFf!aMfpap3v;hE=I3+c)!jnSy@XIer6)Co3qE zB3j)g-@<+~#hb~%tD*3uQ+hPdqhEos%F3IT$45@aLRUin3c#P7TDuOjX09vgbG1Pr z^ueemv+n!~wHqgwPFKX!oyn8drf+O4jFhkW>c}|2W8&+u>JzV}ldnznjP$*|S94WV zR3vXD}5qe4#2b!C{+rQomN zJN9?&qYvz5v2jI7o%JV=%C(=vX7tu}dBDN^lrHe3@f&d1T@Z11Cf>6c#}a%{mxm+x z4)w`-`TY&zl9@gAhc5lelez&`I>JdaI$RPqyAHqvhkt|BfBFjMEl9~AsR_}cXWW_U zC4PZVi$Hj?$>c_eztdUxyKi5V)K#Aj45D5Xn2ZgV7V=S{a!=H7Ll;;fET%l-w_qw* zgRU>Q^cOVy%r}+Es&Hg=%uLL@R<@e7^j6}RFJG*i!@hK#0y}_qJy}fb;Nxm>;!+$A zfm0K(8%8dC0=Ke=4SFTr%*|C`Pc zxgQ!97L<_x=XJht4L1*u^5F2rCuK13!lj}ozP>YM>mkhg6DvC$O>?}pqGFytJ)~MR z_;^(~{?|+89<`;Yyt34f3y>T?<5w71%tK(q5m27hN7%21@sGW4NN@uN#40j}Y4yx$}8ln+NJsJ?hCA&#=%?)vIpHMKjzt z;aF&C>%X#St$3lE1(cKHu_-pE$*lHHt75GP9h>W+vA=~S)2ZNQy1cVUiMU(rTm^nk zTo<+*q0KTqo3;&}HQAUeYqAdY)_=7|O^q(_sh)1KMMiy3PC3SnSKavZpx*{=t-X-G z#RKPN9S9VMKY))0JUjH1a4XNiHzS9#qw9iFszP>;8QQBtv|j|xpWnu6e%zJjFTeIl z^5B?sL)lv#IQEU2uH68dOnpEDkG~wCUWZoax&f8Ppfk5Q_*bK)5 zul-5Fc5G1`=Q4`dfLk%w(Pq)JU94%kAn(}^Vt+12J>`!kZZ*c-*v?di)~0__tDgm@ z6itok5@@c~KuW~HB6#XVfEpQ}~W39c$vyqmSriV@zx#b8~ zs;S=7C>)-)G2Ku;PDhDDgO0`BW z*4-L+3}c>>Oq)5ax7>TcF;)7G;488w3Ae7TCjBHv-rt*!^d1Skx`t(;HuCR|owg4$ zOlqb4W<_kDA>91ZfI57uf##xfi3^rw;Bzy}u<|%{Ks&-5eAQ!&yH31hY(s<))BC1` zeAH~Fjn$3f z(;gxb#!37QYS26b!DnOIR(N9e4DW)vr*t{F-t-zpYD&*R1i30Jxm;BKRk2` z%d2(EBJC*hIHA{?$PjZHeg>AphX;~g?o<}S&U{|9AJq0SqPBW@!*xn_N+&IyFWOqb zb8Iq}cj=7H&%m5WhX@$;14gfWc4s;yQva(VNMLn!kV7;Zb4-T)Lx{i!*4S1ZMI6!V zv{0r~G*)rRD{4w;`dG<8kf*cM_X5KWwV-De&!f*;A)gP;dog)9BgjS}fn)u|qn|@d zc5rGIspoFn6Zy60EO-S-o!~)K(A50&r8BqA&0ljE$iUyKV9Vm-^QIA_sVP(@b$hvu z>7Wd%CB*7OPfk(roFK?9tv_-wXOSk5dLH^O{*9_wBD*zCHw??lV2j)9XD{Qb(>SM` z5s$S)FRs<0BE*%Cn4M_@taZ2z?bMeqZO33-jO<+fwO_o|5Xju%^Xb%0a9uxL(Q}#{ zipTXF|%) zOuQ;KX5sLzW?rKheq9_7Ceg`r5mqE%jm^z5nAGSbtl?7{81?s=BwzOt^TIP*o;Z4B zy&G>nJ$e|BqU;76}eH^#VZO|RbxfVn?`({?vL*THFSd&@Bw`M(c zx!t5VWy{PVvhJ$eu^p>3a_bz78q~Qx5ObU)rPo&t>WupHA9HG=POU{u&EobD+qfS+ z3wEOBUklDIjjM;j!e>+>p$gZ-xNz_>r%d|ZP6^Pwa`^}fQu zq7NayYw$(_&6Tc5)>A_?L-a|vu}|;2HuCy3p_+?5srza31q`!~Uh1HC#MAt*t+Bwu z9yvSZxB)x$qHlu-$*vXFkn9JH(1kKoaM4_0vWC`g$6+@5mX!H5YQUSTysbJFy((Y>A8v3@dM#Z0Ed0@{p_J!XW2& zL6JK9r6|{jBcTtBCvSNAg2eLU z@M4$d7)aoWC6?GBejc6!F&~%Q`PJLl`-8XYJ7&QuJRet&0;{O5CKm1q2D*)2oA5 zq8Y#z!>mBw{oE}(mlwaTAD=%W07sg;SO&J?aJT^WaoxbSQ!8QVC{mkn{NzQ=zVmRT zO&+wP!?7m8Z{U7*0e&{*=xM&N#E;6Qob;02@$>lgp&7oM;%9lk#}jUdfc%W{qUQP& z0=ICaY|kbu)#9Bq^SN^eyz&qFL2}+A4M$porGl@{5|=)6uHa7c#4BJiLU79r-baX6 z=7ILp&wq^3wq9vHZEMuVCeLP>dTYsR+jN@AzC~J;SQrjC$oIS}|mf}5| z?L?31;HBC=*8>qavh=%?eOV|-g52Cr%08JZiN;8%LXmKMo~EJyHrQ0P;w1M5SLrLY zklGW&(h7|zHB%}Vj+d0ZlBlCR?Qg8hgZCSdR$-M_>#RJ#Dk*D*$Pj=VarZ1ePa*w1m_SlR!4^29$2RCws<7L4X z2?GS>-=xjgnCh;jcP~d;(aNd?KLS+X?n95OVFS{KmWCXg`NE;r8P0LQ0P2PArM44~ ztjmWbe^h$pq9(we4}#PGuZ%Bp@`Hi*3d6YVJ58BeX1tL%WHPLHYgW8hm+ywVsafVO z0I$^H&@2bl1s#lfKX;yS_e|B`8RP6$mT(ndm>L=yd0GShy+qaA`8~cIcpQPr7$OPAWvO}>9vxmEu8lWua3(Vg3 z8aQtK0smrPyxo;cY%uPRiW0T|0Qf*+im2c>SCTrvSDXq}C^jp$&2T1h5kZZ%UcVyr zNe+&bqY2yD-fnr+ffU%$n_CCaic-={m*8fW*FU>i*X5kyR^o8vfP3|*t|7-8FGLJ3~nl` zg;ug(hX91l4xYW_)VMwijC8ijB(_E@{udhDjycX)N;~oP)FQIQ5ZLvVD_0t>>JEIv zJ*X73HV6m@c%~5#z8qqAl`;$7s+<$QnQT>Bb8AW`%Kw&r{CL_`H$5J_5U9h!)m{N( zVncF|-!0UQe`P9uVb5rj3GGM%J1qf6y4*ALzmwr?z9%~4B@gbBzCQ9d7MB>3%YQ{w zCLLLYBi6L1=9dAlT5OVCV2vhScFSHd;P@tBnV}NIlQ9uwE7-G1rgM3wDQ6Gvk|i*r zQCI1fY1P4T9&PXF0M z`21H43=G|$6eWgv+bmLU#@tMWk}Ug4ZrNowDcHZE5jLxivjw>o3GFV?jaacTy-OIi zbY|`NLMzVB#9Sdwue<->V3WpVhiDxOei@hm3L0^r$M*K*0!_oF+rSEG?L7ekwIA2J zm0CdY#i8T#gZ(T{S8*Qz7v4oUc+3^y3>cBq#rvS(ciG zA+ihRKe&aeR9NQD7b5;opfJVDn!>NNk)w*g5-)zg^TTx{h(BJ&AA3@-UODcG(4#zu@ zB?xrjHf~0@e)Bz8hQcLIaNN3u5kw^vzO6N|g~yeHY{0hxdhZLbFORov0Gror@P{Ab z?>~t8U#U=Bn+2Xn2F6dl-J&d#eGidAmr0k2_f-yZb^Vj-mQ5h4rU8dsl;mCTnggtZ z1+D~^!P6SN{)<|i*Eks)RKU6&Y}7x`3Erk>Q*fc31kE zvPhBE`@T8>uy|5vg(?c(i|J8c{Krlt`^#w2 z-C`R1j?Hj2{@02k&%s{I^0#pU*9mHEB`YO3G80&xMyVN958T_W^{X=vjJ&f_WKMu$ z0i6u7`r3soK_f8f4G@Eiz|G_-=jc+$y7bt|=?-8Aq?;8?VkdzkpMEF$o2l=&Fp)@( zGLA;6q&buJfHSq>_~rx>3i$-3(T@uw4Yt5b6uRvj!~ZJxBxkQMosUL2BZkZacuw}x zl>v@?lqnpq2g5SQcmoJ2n#}j^wgzG@JzoSmZoasP8*ZF&vd0`FKcKzW~Q$;gAPV?|S>0Tqw z(MsWXZ{SF>PS6?&xu$&K=iz69cifVckp8}a5#R-h^WE%%WC%Zq)7wQe#dj^br>YU# z-vMfA9iVIsE<+IB_aNbaLmFlxrG=7aQb8i)$e|gOO>(*Wi5$RK&Jpmr2Hm>?rHBJx ze1qZ#a~|)@QSck;*gSyYCP1VTf+ny?Vc$XFp-?x$1M!DKxf}tgjG|uPjBG&O>=&V% z4sL0D0l*rg7;_Zehf4ke7N+OL%x)qGXhR^Nc_IE5&7e<%v=$QVXUO5r^0eQU8@{vk z_pb_bUEzYo_@5A?pY+f{kPlvv7m3f014kp3^TIZBgXA)xf601l62S?KmH))f0iKv6 zv9pb=0y*|P+$h7DagUy~1{D{M|3?X&p=e9+I7bFxEI_IZ92G0kqf5C*zYHX`!FQ#_ zgLg>M&WN*{%B{kkm2}XF3~0v(;NUhvasiO+;(Xw_fK8bqTTIJ`d)A)0#%9BMZMfF8 z`#5g=|3osml{4V@hep5iE?=kQNb8y>=l_9$@G)%4OV+Z&w`p04>kgb`!bCA^i-7P6 z5Cr!?dM8<=$RZ~TZuWKH^)G^TW)@HaaEOrHJg}SV#)rQtW}~mkb53(0de?|`>Lup? zDFIFonBxE_V=|;?B_0a=1s>>W#Y!)5#8Ibh(w#{nxonA(NCBOdvq7vrwvPzS*Iba` zj6`t1gyUPLOy6B@Z|p(5J>e_p=ASKe>ZC&J1#}18!A{_ae8q~Y(N?9~HDH!+zTr>3Y#uIpRhIE1F8fdFfhU0{wTQQ!YR1ss_@|8mDoO%|9ta48`mV@8u^H4Sq>+Pwn^ zLv{km4%nHh<@#6O@aGr>oTsMY0evv(5pS5HX#B50helxk?}hBmABTf2TmnW)3Lhtv zTl;!@dtVWk*x+g)-gQRK|3($JwnnuB9JeUi(sYS4CCJR>t zRVUP?+3q;X6hHS}FlilOi;_H@wG{P? zDv>?u7=@Y?-?JQKOCGhiG$|6@7k^AxayVojifjE)nObVIq z9`)kXva;`wNew6RLOoRssrGd~(@zaKY!v}9vME}84_T9GLJDSt_hg!&e>?F>xFvQd z&k-I=Um+7Km)tBfmXY&&Ex=a1%M}YgpLR-}%O;ibwj5rVTFbx-(X`59d+6*LyfS_& z=S{MBh`7CZnG|we%j&wD*`RM-A7vk-)xVz_-lPied~}461?WJFrs0w#g&F7V(v#b~ za_W0U1Ez&(WL44FZGr=SYwiA2L5Fe~>X1g>tlx?~AOQrQU2s$(?A6D8Qdl+G2il2amR+%q~GL&*YlM#q8>W3rsGW_*AcOE0{*cx2AU3CMY%YqbVr0P}5#|#Y{ z)+SS=;M#2BE4SX#&}l>FAEvjy0^|vbWI&HUx-NCi{XRVO;_GaZn&3ajPX6cDYC4o1>K?29 zASwzp3PJEy$}4n%^m>eer&=aAn$02RDAFuW02kJFlt=I3im+#xWNgyue+9XFVLJ-v zd-MFxB$6d{>n@xM4}FPws@SXw_fGXM!}vk}2D!qNObC;`mCM3#bb?IT`CsW6jl2E9 z4kO3zZ9Rp}%M8d#A<7}r?$)@1dVeUgMTD|das2eb>1nnpuH{=aJp~86RiScghZ%Tx zgWTlo$g@jIZJ!IoV4J?0wvUR!cM~n^8YU))ULU8{@)(Llom-jf-tMXQcg7?N59jQE z!g#iCt4^h>pY!0*3+xh^;)2v;@B%7VS|)i^rCKyl2_~XB$~%BaGV=|GQCTZ;F(md1 zs`=-oxG?9oCv5I;E6)q8VLU#%)bG8v{gj-o^DreG5l{qCwH|8cwB9w5FU^t_(83&d(k_1&qco%U}6IBv$MJ`ZyO=T(}!*iAP z3U5*b5`%rPtLT?ik;iy|+)#;7SfjG7-uI-I$2#SCBUVqXTs=5YlxN!&USso7b*{Xf zGuRgTur!G_a(uFv80m-ziVNO8b?U&obB8;PuDh`>97MS*#s$TX1e#Jd9!K`0NYNNP z)RTR`Q7D$+D{&Sr_s_WrdM+A}ysHU_L+p54>`vKmY4<(5*=sAJk5tRIiNb_v;D-$b zL$gSE&}LI3#f*)JU4x0ZCpLqBaV$7NoKPE6Y4x&AMv~BOpA_d)abXv?YE^Ia+LaX; zcCoEy7)2@^9o59SUCW@|%|T75JskI@ttmXXyaYKY_;6-N$w9(r`AihV37d#IEEagK zkY+x(2%c%L8HVJ6pS4JbTU6sC#VTO4)ZJftQLm75G)gq~a@b=nD|Dr{pQR3V&UDw5 zH@8(_He&aAwA%BchhgZ_n2DG$;!-I50bPVA-ZemYmh9SCuU_~nClVfKDELs#lk$WL z0|Z?mjlQ#++~O>b-zv9NaqaiA2$2XyVf6S%+v~~1BRj&q-mEFMRHT-iW|t z!Yu*cG3wNC+G-~G*?cJt@v+W+_PU)S;nLXQ5RuPZ!E31p5y(1A4r#QFcF&&Ygf*J> z`zbB=5+#_{y=cM_^ku{b%?O<%m* zTV$xfvM7bpzO3BT?KxUgy|QXWP~Du)Z4KR3NR;1H@0Udmoo;>lMlpTVy6JTWs{|}8 zXM^rAw}NsR$8S9vl|Q?y&v?Wc$!eZOYM!p44Wl8uE72S>T>2z7+2M-_l<|>UjoMhrisoXOK@s>H`V z`a#U05^vsy#+GfG`JQBIm0jF$5P!ur=i5xPJ!OY70pV{%8EaZD1P96M>1%zp8hcT> z?<1+xh~fKCB7AOM1hMTp7MTQz?0@IUqMUd;<(LkNuZN zGy+e%JX5>!F1$5CyR#ngfbhtvZcO%^LEvFk_C%zk1L7ES5E3EeG0M1WS;(tBYSJ%p zBRqhoy#K;xE-vv#QxhXo>bkf5(h0x|pb+?+Hr&I-nwVoTX>8GTvj>(t=wwLm4 z^BSAA>C0gms}G`gMH~9eQK-Q#k8yl-!^`urYCpJWS?Rdwgp6`~CkH3xbJ)lbW%}So z44q;X30+xru$^}xW<$v*EVeT=3f?b9@c74cRNz}d*{vaHpYkUjR7(GhPkI$ zGJjG6${2V~)dRg=cvfuY?I$DZy-%2PAq$!dBit`K5v^a8+9bZ(wwEF}`b2>e5yLFG` z7*#rPz4qC#bk6q9?@;v##gb`f1S^^pf-rj~N?>zF(mA(n8xqb8z+(6V>vluc){0mr zDw1yzS8LeQXI}1$L`Alq8QXrWf3K?q;+5)eR=1|ey}KvXIFYm#R-io3BKOY0nBdp$ zV{d(q-EXrE(K_dA!s26p|D#~J1cd|MXl$ny?w4hu_aQt=jZNZi(4_)i^}cp~#>usv5k6#4D)IfEp+k-QCP2-ob$vrgfgkn#^rqK(zdd){;s zOBJng(S|(>XZcTc6@OQWNlxrNa3m1E*|*Oy3#+A#4T`Awpz#)`#Ljeh`za68R3#|6 zrf7AJOD?!oG4FaHt6&uwC~-NR=Npeh-nMVgG45#v;k+Q5*8jL(dAlsC>>ttc^aIxg zD*J`ZwWE;Nvog>w7Bw#6MpA|w*LEYfkGYOqpI4gPRWF(G#qbv!E<1QO9X02mM~k;E zK40Z!X%g_5jJOU z?hlbx1^&-x>~B(DiHSepSDzQX>(QBXqweW#-{9LKx3PI2a~9MJKb&gj?=pk+rj{m?%IkjKdI@A8(bT&}R9(V4@4SJaEf;*B$46uq z-mHKSph=R&VwIMjL}xsEqb8}xIgapsQ@GpP02qp=%7;co~Ms2TAD)al&2^UqEZ zz7(|wwlV}6O%i6{h#HGGjas#jDCFTGvC`+uI`i7?^U<6>V|UThcJunt$pNA#S5!rE1IC?+sRpAVlG=~>wy=lGwA$V@8U0>Tic=gX7bgrIH^&I1Wr_36WaJ$39ASsXf*t#*Q`r!C=MXOi! z+rmP8YQ9A8{dW^V8k;g*J5+)YPe{i|K94TqQKSg+YIdks;- zzBnNQBjc8n4a_j3%MUJPo=*zXjFXK@sVYZJ@TgkopHl66H*x0~Yk>jh4<#Fw>hkJ7 zWrgy-rrXT6Chh?rEo40D4myY%2Am@}D~9PLe`Pq{Sg(gH=@H5{BHL8vNnCn*t)S5~ zFruY)meR=TcTSjn>hpNg@6&{Z(Ti!EsA>(%hY^PKefP=a9Bc z0r2LUrMk4mmg<{Ptvq10Pqz@(W9=SnUL~q=jg`t z@y#nbuq&&gLC&k`TbBtd+nh*_Si;hoYC-k)S`PQItq<-Po(Uu4V+~9;`mHgLK^DR~UGcsu>cn{*+~G_4Ki9%mo9XV-;d zblQ&9SUg5Inwv##YIFfcEK-5!%fdJ*{hS;p?BZ3biE>?47$<+f6xBn<yrng=Q>iU|p6W&~xut(UaWD zK|pJix7~U??d?&&V-r^sM(YiJ8bDb2DI=1aA@4zc@nn2vg*O+=?M&}pnBnPOc~FNQ zv~FpYUHkNMcOq$ezFKA0q9KzeEMYqYj?Cf5uh-@33+)DYooRC9+*#k4qvl(;M&|;R zA_%cZ)xRWTSr1x`Gxk|O(0k#dVGjup~6251Szb;%Z;b*WO%|IvU^+oT#T`i}HJG_@Tu&c=1vrWtp|z4=xC zWMMsO^jEN|PHKv7%nq8=CN)WsNi+Y4negd=>=`n73wIt7Xcafpl>9{O`$2k$=Zt1Q zA8yD@qAdvr zft;+`raIt4(&5Fau_4*8fTC0mfGYWAI8#T3i#3g72$uQBmMC(-#|tVGgq0s<0MTRy zI&gK^Ce=aD@yaSWnZRi`EQ{@gHovaqp68tjeZ3(si8*-NdRsa2)~uq4oX$S~RJrU% z-Sd>~W`+}?$}0jXM2&vCD#MEpo=4yPxv$)>lF&Bt1|XSXwf(_-@8h0)H>5g@Yk#y^ z-w8u(v!-MBFAxY{W)ZUE!Fi@CbC1)^YuN*_L$4D&9C(KgQDUNn#jQ-isWvV7zjFV>}s%K7J_fB*hH;ftEYIvW=FT+7l5D8oS0K3NY~O>r_n^jF- zu6rlBW!o*U<8u&9g|YA$R`?dVgA$*dK)*GQw5M|^hrD$i<$ z!5x&a&_GCnsQ___{n=+w=_R5f$V62bpyby~2&ONE64K>54kqsLIdKdXl!)o=rx&Ns z%pIAhhHF?jz~uz*K>(rn;z_K>aO?@doL|W;)!2u6p=~HRODuojNmW&~Y znKx5ugV3ZmGZm}6!fHHGj*cIOE1DT{91!-_gH9!PJ%o(Sw7=i}5G+ld$f~TY9T&fp z<2RUM@@i%`Te&CGn!7t74v-C5D9=o1Qe1J;H)ii~poz`#n>pcF1yoAy%9E=Yve0cO z)E!{7_Z>2vg-$?6yWvT;Aq6>QxHj?;qj)n@#iAFWuBFGDfr8nh@=-@KqNXq2xhwxMj;mleP9WGn`wcut~*N8b87Nt>DP70GqrVD9%4D6VKwFRxk3O zYWkfN%gRGx?<&AhZzJb`lpq{%4{vQ~4u=3%I>x}r7-jnHXRw?iXe%(771NZ91aRj~ zK#uqC)tGyoS-S;f+v-?E*QkT5t1B05jC-Vy7#cGsFaZF+#G&cAlCmoRz8!Xz&Q&vX ze^TFJTs&y!gaA^2Irs|4YnrQWf7fT7f~TNsz}o5oy3M)!UMPFu6@~_W zh^WB;t^+h1ToE$l_)DwW)!!v-r<-jcnZ3mQx8bD=BIv7c6Q?*A7m(CrTn_*@*%kc$ zqhK@GOg=E$^%EL+1u%7%K)m#Qg4V$run$Nuni^26)U$wJ1pcS$A2#*H+R07N=_r0) zxN76_zxBV&KT+PBIiw9@PS-gVn5BX?6y&5ms7MZg5=RLvv|&O1zaQt>!B56Z?|qm3 z69~Xrx*i(=;Gal5QeiKGBllN8jM>DiD~^m&+(t=y!6_d-yt5!0AABc zAOd_d{xxOmBc?EmbOWq8V;0`GOR=nSO*xU#zrJjutN0m^lvPDfeb^u00nHV%xGq!1 z|NU&8l9Qh1Ek19_)Zon|D|e1aR!PR=z%Pd;o?P~zNO}` z&j6X4t!t49*h&GU#O2k)hEE;D6$XonE7adka^qtrwO(4)=JLs1@l7X+ET zquyBXzmY-bo%SCSU2y5o!p6c%1~EV!#06R^W;+tdrZ@jbGzppT##v`H)!kABvNky2 zP0V@Y{Ja*jWZZ}L0T0!fO_IRrA%N@SId%qQV^KS2De!I6W}_!;?JB}>@Ec$%Ts!Yx=H2Brzv;2dDV z3bnTZ%e4cwwdMHs9Jhj;15H)dRz+}A{2#&lrDlz6yHS5bC%li8zyqKMO!T^2wR{p4 zDE{tt*31HXV~DnXm0vel3?CrS!p2y@y@)?)VVM`bfM4H?xoK4!d)c)%uKbk)WdtKN zu)JJt)dhZw15o~fa6Aj7#Wp~!?DvGr%-6=A96zV@0*XvXZtDnKa<gkla0@IuBU%A_Ut8n^S^yFO z0}U1ebV**IwaEa+omJvgQ;Pl#n-G-^+g=Jd>0e_gJK-x$d6PF+u~g$*FcW`Le$aYK1W)p36O%m=r9zyw7qOG)`? z41TV%z9U1KJ89iA;mP-7{|-2#UlT6f^?k2_2*wMnj_hU8F@hJYNBy@^UKjpuZ?Bvk z?`LK@U-I*zT)AL<*@-Lu1&mHZ+s8Qpsq$KLX|zfVbIfAb(ohA}9^yi`>d7aW{etTc=%Ia| z3UV5WQpFddS(d=}*bf3JP;~1_vy8WZIM4#VNy)wGcEjNY%vwt1ON|tEm8MWD`{VUC z?r2Hf-j)aACR28|W6H5N;37T=poeri3{NZRNs>M*PqTZ<=X!6bbsBHd2{)4q^*WZqPf-dkE3vnolF99j&x}(i5vo3wIZU-*yKIz2hRqj3N}k7E}R$d|;?L zdv5C2%LF%iFM1Z54C<5}Co+(JMH>5$@=oI!FB%qlL2P!2*jnm#B65gfU$H96MayIi zsQLMLYxtRo^b)tQu}Fyz4|5~gTB7LJbf@Bgb`*FF4$v*-f`I+<`h%R)Ry6C+MY15b zF2K<;t$EI*AgmZ#(k%%vNfGM(aL^;e3TwnVAG?hle-a5Nu7Zw}&|#gnPgLX10cmT%#g%s~(<0s_i0&?!lW0PS5a+M(Kmw?OYC zAH2sK(3zmI=H*2O;?V%HMQ6`(>*{Q9(wouIzXpK;;opdpG@ya6`n@voe411GWPjx{ zo%(oSf(wl#%_LnDw|vVo9hRh*#)-Tc-5f1vEODoIOK!@ty=l@#OVOL&UMV0{qC%iI zdx=TDn^;D3dkTxwkHLWuskaq-(r;1fo`lNQ%vL%y zEBj(xG=D64P`oOk-EG}wikdd#pRM}iN3+pl7U}lQP@PfMx-yNiI}Q&Bzn4{~q6B0% zvvQs!^s&a=$Y#Q#COi@5&khT4n=#4N%R70`@?Hkzm0pL1y~nV}fKH$Z&>qI~CJF`G zT#EpW?lk2K3u{`i5d5No*e;jKaC(R8VzirhHzAt_i#nonK&YkoJA~bU7t<`$`EWrR zA)vP$E23s|+&8pxZ)&_^=mK(5AGMYyNwlHjgKjHoLX^Ue<7%&=i|&a# zw%0_Rma%^o`_=LC^gQ($>QJBxElCN68(I&OX$hE(Wbq#BPU8KA+jeuo?<%Cmh%27@ z8+SLhy4Tjq3?>w4cVkcypFdFKqSfI0_s2pVR_P}Zh~@N8_~-!86gbvwd1~cDFY@P`S6HX<2t3 z<@PFC#+t93Mr?&60i!x)GF6Ni`lO5hCM)n)+scpL9$q+aWTu*10s*@7j8p$;sVKgWTD$nK@K57Uwv3@RRqt7p#NBejZxId(WTkd!w!t7 zf6wG21lc<8JarVG4CZg*v+hAJ=fdEzM?II(MLa5Ea$t@m|)Rc2dNRG2NJa%((j` zE{htSD#D)MfO&7-SbWzAHr^E`_x9nb`}+&>lZ?Bp&bJ4YyK|)G3X?0j7xf*f)4aK1 z*VY_C%ikz(uz*hLSFTqdtXa)7kKS z=PYI5K<2Vk1z{l$h}8^#h!ks`w7+Hm629QM+)sN1Al|P0lC>q0)Rxn9LA8jIx}ZzO)&`uF_hwuZJ$$X}OvM)DwPdqwFXvdD&RmujYOZn{JCcogL5*m1S)U+^C~yoTQK)%_T) zW%Tgsi>uc!m0i&M876RA`=Ws*6tDAKr~4{O7x$b}wy?6l!XLl@@a@2i3Dl=t)Xt8w z@a)$pwk4Z^B@y zzlCV3P^1}V=SavD0(9(rCg0nvF^Bk6p?GKP;tWJliPX!2}krm*AhA!nV&K9 z{hmI=r%C3(M{DJjLjy`>!A>%+>Xl-$fAaI26Mtnf6JLc!uPXQ(Jrcf7p}*tf!l7v` zdlZqOIe+1;F=z{4`TJRG{`*1nZ%N2F$z!us^>HK6#&j+Hh%7p;g+z{PuntB0u5O-# zS^wmWju@1n$zhyY6H_hM;*0gaONB+xaa89!K@L8_?@C|5k$l+MZMjyxQ@R^kFX7DL zk?gx`CX0&@9_80DuYMf-dv#=z=w*Dj>XA*`8f(Lw7b$w`EqTB1XbJUf>)id#!!(t7 zXmQ;0nq}wF^69Nrst4h4VwX9(ouR?Az*^R%f&IF=U%XZPVxUbs(a!5h7;D`vef)z_ zUHL2OT>TM1Mcv|t*l8^5-JeBWza35VIMd%8{D=uf68CatK?JHrQ>p(Kd+*`Z)E2#q z?hu;Ni}Y>)l}>0J_PQKTbP z`dysgyKjs;?s)&fJ7b(P4v_4<)?9P0HNS6`)nYbe5bUjB`YAI}uznX#Dilblp-;-m z41Sg)sya1x=4={sqyT1K`VQflRqP9=bcqITzu>-a0 zl+#Hss3KRO-2NVZHhXT%a?Z^uWv#jDqi~v3rB#z>o_<8Y@>qOzj+oiC*U&)=RaENL zu8vnikoH<0sw+tgX8+AV{kxQ3DNAe$?yAh9?@5~Hlg&=cUqn`?6#yhj^rf-#eI^!#kWE!!Nlh7$eorr zOHb4U;d{~~JnLQ%{k}Nl<9;fVuV47GxnFvI40?5CXW+Qc{r3hat7G;FL7YQZP;T{l z{g)>zp!y}r4_^VXAMdF}la;hCl(AHp;wJVC=j3$AgR;_m3W?FKc;fXu@W0Gqe&YQf z{+MhXcHx%(QN1|Vvx`T^ztvr*eN#&qw`#aub#P#bN+5k!sbLWCY5y~K%>toJjGCOx znLd{*E*W=CH*XR@4fY&k zT+RE~ni8aTP#xT=Z1<96`Lja$_MM4hqZN&Q>U=0%G*!K=uRzO}Evh!%{lPS0X(X?O zsZr-F$Vw3)kx*{y#;C0ae@J1nS>>@j=N=W^27DZ1nZ{3*luvl(5E{wD)5dLKxI?*< zJEJ;EvT@P%_V#WI|KmdrC8vmyzol$k%Vcnipgb(_6Kj(O{T`{gq+zI@*aIqkg%?leOjTW7~5uB;Qqf#S? zZhN?XZ#=Vi;a;cm=QUL5C!t3{vk_mfgGx~8h)Y=!Yn=TxmX=1Ek2mY2Hrmgx7D1ba z5i#a9&kWhlH47}T7H9?c_a;XKi+k%GpCWc9`)u#?pc>>Su`bosgmy;KkPL3slUc zRgmX5D+;9}K;vjZxAZN#syg5`}9_bhk8|@o>6*n<@Df#XugH_#A?D5~vKy6O) zneBvN*^cq&)V}Q5ZH2BZ>Lr98oAY(#u8nAezX(>Eyby{|p!M6tdxf@TDGAX|g(F+s zj?GgU&Seth{D}F9>v>{~G3Qs`1vKqdmfga=dtogrZ&f;Q=|TRV=ViC}m*~Hy4pL|u zv!-X#mNo)!>(%NwALQKxpoD#S@#sLW+_4Jb_E5Ei$ zA>d@{67_3d))88h?o+yElhp*wnMM43B&leW`C@d4QmG9+(IcAYaiT2ep+7UHVAgD~n^7G?I{rmSDX5jJ)uw)9i*(#7jM7xd9rNh!Rz-IgNj=HVqcaFT}A?pjr#U%n&TmJ>I8oLPa)X5=s$Cv)Z``?ArE!|^ zZgh33fnl}&YT$O%K~mYzH2oAC1~HSQ9mA4q*{se##TezqsDxl`31vS`Ev+ti;tZL9 zl$*CUbRnHOJqO2Frsn^##%KO((^Ji(_!5FIN+>IWVRJ*7uEGh-5w>>*X~4T)1T;lm z73yk<%ne1c(-yVBy^LHKP4O-ijnv8>O;!$@0Pw~vLaV4zUnY5B7VPb+%pK+~!s&_Y zkHi=U#kOA)f?b7^nIp2VemiirU!)2gGD%9jA5eWqes&+PgYC*PlmZVt^k1Gj#w{F_yL7~v0oMFs89&U-J+*7b zGUHO}&wqVj059&ioJDhPaJybaU!ni>Yc=Hx_u@|w6!V#l(VfpSbm`k}YcC~?rv(cs z2O-d$1Oh();px+#5(#FH^4%w!3wKLhft+Nk6~c12hQRd2jnG$^E?YcSY6v#sRcgT%pD6z|l+N3h?k&1k;(nRG9TrW6PIMDj;h7+I-?02JCFIi6x02L|ARaqt(49VNe_*H;|a z+TW-FVg$MMYIImBYty{IQcA7)mCnc9b)dgg1!-n&7q6|$csD&rJ{47uTH@%c%J^X# z`z3Wy?i~6`atcUNxTFVk2ov;cootsk1ffia_N_P%i}361EYUa@@yd(q%EiLw-ic9!>gf zK2-g7TPzJ$6%e2qQc+3kdLU*(8wxbx2|*GF*?@ucWoy5y*Gn5KMB?`ss&vH!)}(rC zSeW;T{RF~u!L+m7of=VO4h1s7y^v?_DDPdkBx%?`L@r~VN`TH)LsRWf*j$QCI3Ke7-m+z9=0T8QGNH=8_xdowaLQUj80Fp$EPhJi}n?MA|g)4Di$Sh)|zX zPGZ|1r8c}S1jOPQ(w{=mxWNxZDEu)u3xD9u=V*0MBrw*$UvmHajbBHjmtX}}?Q6pz zF1n+O4Pe$~ zN4CPSPS8JIECn9+ydt;q3_|vq<>Z&@<-(*FL4Cx>YRy%HGkQclm&-I;7y*6`LSSwmK z2e+q9I)U~vUpZUJ%q0Wq<3kK*%!O!3{bnt2VR)* zj=WKL7(4N5u+b9Tn`EF(pU7uG1@mJB$wr^u-r*E?eJ{{{efLR|!T_^DedY^GnN=I) z1^NO5p%%De!P*6Z9+BhE-7(ToqcE{DvN%K;>o%9Wi|BW}xAFIi0x=WjMZMh4Fx3u? zF-~(>kv!!R}7 z=~VBK{|)AR78+j^J^nlr_QeuX^V$3jyGW~8PTGjZvEo!;(+tyl++3r>JI%eA=-g7e z3qahA`Qp{~kMV?FxMH*Sl{5Hvr4}V)rUB-YTa?Y{*kzN#RX8%aI@Ppb;KcF!Cs3ai zYuKt&UDLAf1)*qAkyfBKun6rqRIqRc6QT=cQIUu|$)@w^+mb(F-?pTt(=KsN2#A_- zPp}fr1#@$lr(o&|jF7x|xGkIiA(hP8AmLF@(D~{Y%hUfN>+A-v-1y{gX`OG>oMVtc zg8QUeO@l+_P$_6XL>l*c7adej?^j4@{pFbVYhpCPZN2HktWtrF_f}(1&dEjL5_P88 zt;W6?n9y>(+%5beowF!(=wO984TaKZ2ovuwjnqR23vF#ey^&EvcCwY?;hfBvgre`+jlz+eu^&%M=A6O7DjxmG^pGaKNc;aI?TMYFbJ8m1%Fa81Lpp zO^U8a=1Ihv;So*};U0tj%$AtVSd3+GhmvW>#yyqo%MAU~uN)blQyq1V&G9f2s9cbm zeuUJx_A43RA^H{fj=&SLVZ*n-UT>BcAK@o5gCY?$2hE@Pvt|!U8+22R$1-yy7EjO3 zMygLn1{z#hi>}YHalugF!=l82rByX|zN8=}mC@(lpl_l1vMXy!HARpt8xdJ^sHpSW zuwzxXZAj3VGtjL_L;==MbT{n(rM9FHLA7bAC=7p6BJo*_TIJQ^+F5 zBcnlKKXkY}sN>(%6}CBo}n?C;;TClFhu)=rU~xnaxaVm}lA4tgSUqT17{Lcx*6~1N)cW zQvb~E^!4RS&`eqs3$YYxgFD}u&`_VbT|j7^mG_2Ev9Wy2Zc{I4)hSBfS(Kw4>msNH}pfH%n zdzu2$?Fq?bt&WY5jVT8e=F#BFQzx5f`bCQUp$z4k%&|0^Q1gNBfIAX?w5#jQ>?})S zf!KY6n>vQ@4hJ@H7w?B=T+YMkkCXA&y?({S6PPwMg-2UF&ZN z<5#R=t`-;sk30U!&G{W~Bu&$O@>zmv=~9yp^bnkPWF?&!+XzUe(?803KZZ@BgM(xb zoF`Dm{_A}6uH;Dsg>JO&1}Ux1^ix~ugTaocgeNagX%4Qv z)!S)1d<6XOVBmkd0Nf)?Uf_{5l$*a6rIP2Wi9Hl=678RO95Wh~Hr)&zd=)*0TjMQg zIn%IZ8}QdYCFuOB5_HK2m6!qlg1dg6w!k0=!XU>nH_qYqWU)QHvKHpJsKjX$*w&S5 zY@V3>+RZi>Kk_|!aoTnE^6EL6;&Mcm-smrHo;J6Sjt!HSmS@z?7ig)n{n>W&(H)8_ zUr8pOi^>xmS%bWsF>DYPFJW_zopv`}yPuqznE&VRL>@c80E%aAdv61jO6L4DrFE+9l4`Up`d^kVD5a-Gzb@i<0#`jnq&{ zo6YFM=9^WGsF|Kb=72n3PtO+Zc`=uN$L>0}BG9^-N1w+_%;E?(P4>E6M1PQQ1i;H3 zfD8JaP^oZiQ{YV7S34VA+lA`*?a-7A=2NHfj=-5Q1kMcnUl5q|8`6zLiMVH`I|=~Z z@#lh0GbaExC@Mhlptt&?|6jOB-MuOiXAC%qF8{J^L;RC75gL!o=u`0$+tvUGnfVJX z{|cYDqR;+xseX``|J!>-`zOiQ zQod6b)g1I`an)yEcmhC2a?&&az%Bp)`y z^>_FLNCeY+43Oo*fHvjp(<5ky*LB4dYNS4r3NKmSRsX%V-3wq*fi!sbP0Ur`fg9== zmFuH%>tHfbw}iSP0jPdx*PM5RC@x?&=_qTpa~GA3Ex5|@@Qe_4h z+BhmCn`!}O2)t{KzuM+HMgTnF*0ugmut)tDXSHCuKI|2<_I22>uf2kide{sZVFtWwQuyXM&2b+)a_%pE#lN#ct( zH#c3O$KbpltV+}Xasi{`_XD$M2XaBiKN-k_hnq*`MOri+@tVu6tBk{j0}kz)jD-__mVTLP=0tTG+YbQ<&O1(L(V z1dXdL(@0%T&UaUbA^{Hh2qgP1xq!{NS0nXM0WdBFsz5g~FqoR2U#sf93zI&x2hG4H ztDCor|R48nC#=?(JQYJi$FUq0oP6MV5hBI)CgRY+H{W~(OE z$j~+iEdM%S9$Eq4K|qkKq9^szUDCkkG(mn0FrWYCqYLJP$f7QQvi$R_OJa;ZtI@H~ zj^21KU`Qj?xBF;F(O^g@Kv(HYJsN><4DkQY&d3Io!jzr%Do}5F9`vK>R|B^)Bq zLl;)tObV6j+DC3FHW15I1KX%(ZkDZSp5QBJ9vqs{2N|ArU7xxBXlHH*ur>6>v=uZ9Jn7hDe5N+ z5Y{xo=4?{_Egi}((ALB5nKe5%;q>)(1o{>9&vVcpH7T)e1A#6yE%32*SBQ1F%Q5Bi z?YanmV5p6GbIUlwIIXie{v>_1LxaUXPpIN{fUi2FR~8wKAmyNPjaSd$BL~Or5~kJB zj(wNAtV8z|@tJ93yb!tU_!K8J>FZ?$bW9NJFBxD5UDF21{IhL&U{Uo@@tFGa+(zbr z##PF54C9#y<@nDCsJCQi5dYAok)(@7g_;3&HBk*o_&MbmN9 ztvE4jt@*5iWk8{2&V(NVb=eL>RcA_!!W%2|Mq@b5ul?^_0PCz#*g_p*QT=C(evS)f zS@wob^8N(KRfOi{%2FlwCRA(62|8b#B$M)Gj^BR|2W2O~+XtJN4AKV*DrU^z*w5U3sYHhVorPgD)2ghRS)&P>ou7WFG)2=*qK z@ND8srxc{i;9TMPleZVoj?Xh}rp^dLZFJ5u$XzBV%jP^Mf(bLYU=ZeC&NS5&uW^B9 z_?XAcM-ylQ_J$vu+`CW_U)=%?bDZNPu@g^Y)LLGUF_0y_B9)vPI3y2SaYdFk-K>OJ zpCB@^P&kQI(8&18cQD~gHR|VA!ypFuKYq{{^CGf_F2V~fPxri(w2^|7YRmHu@HK{X zv94oVFB;0#Lg*ETbmrmK9K^4|TcWU)^c{xB+@v?x&pbIW2pAG$OkMrY9SL){vKq>< z>5?>!pXQs~3f!^5Bu|e(z(4Ik=sgN@|0x1Jk^0!qHgyddNzvJ5!m|;mPvZl6;9;#x z8-tJ!^hOJdTN-hMCT=H6()v9o2roK@itQ`fJ6}46y#fuw6={fU(94XoG<=q3K=?c)+t*tQodqM7hf}tLoQ_kF#(iR0rWJ`x<|Gn&=d{GdlYhgyONrB|#-nC7W?wtbL_ zm!+}pBro~)pWficO80t6k%XbWV=S%Opi(ZbIn$V?@f&%mw8crB>Uj7N?23b9)|&)< z_OWcxZv{|*x=9jdpM^i%71K~e<7FZgPVX<=Z=QIZ0t4ytz7qR>p3}k7hM!xZLE0}G zwaNl(Tk>OUVz4(i9H`zfq5hSzGpI;92*Rjkx{S%XBU^@|8<*LpYNc8^YG4ob(+i5L zLg#Mr(K$PI)b;d|Q9g`QtjKv9KgV=8fTM3va0D~Y`q#%jR>RIBd_cy-x7#$ zH?UmzENLi4^}(cw#v`a#wqOk$SSPiT&1lG|;K4C+Sr3cw_zjF|!#!}nhtA~6SP#nT zY_K{H4P(y7#R!>KP-8baU&_E$SUwd)5s9x&D3MkmP@kAp#A4$`UNx(!8);^i6fKWm zMJ1FTEPi@;A^X(ekSp}b$H;2SuTRa|Z{m{q@}do1Fq;~;v=IV{_*k&|cpNe!ca0S~ z9*T-B(#^-npUZw5Grqy;4I>81bo$V(Ah5yXw6kaWZ+r}C{9cutX3tL?#B9R1B2wbd zqSrR;&z$D;Kcany0UgYIcPc(gH`cz;qN#LJO?FBstK7NOT)KXzKXI@CU*=|?dLDKRN z)KqP&keuLIFlPxKq1Abj^DpNmJ>hTQ0>8hC3G;ZVEkuc9^YCLQW}oJs#cU=^d3*ht z)9GL_6^2hezW;Ux9lU(<^`o5W)%%S^hHu@k-ac_b?qnmNu=K2o3b9`?QlQ5pvYWc1+QB?q4oSK3VK1}ZL7jmfUj!X)+(RxOj7k9qf1dbG;T*QB9w4KWAiS8wT zKHjn7u4cn2UjA-tKLw8nzjmze%deRFLkVi@5c&4MV%{l6$Zh@BdBXx7?%26UJFq<= zqWVsW5A=@}TjgVYn+tMN9XmXObyC&+M)`c+;gPv7xojliSf6!4N8p-pTWPKY&gh&n z$VJ+My!r+QL;k!CUz?cQ5a++#ww!ltsvo$;6iuF4Cqz5T6b&+R(yZ3USo6VlRg70) zEM!iger@G(+*1poTXEd4{;ONI%LNUd8{rRVEi`rrnjGcvxa;TU)X>7{U!D*YuvZ5k zmV!mG%}!XZnbBHVAXb(BwY9&P32#@baWcN5;vDgw$~6f4}vdE8&ib0R2vMlN!=A(S8@cUsJYO8+HMW>+W*-zwn+%V_@lL`Nh@( z)aF=$pNGDHE|(1rqHDYDFcMM#@wHoKtHNQ3QNRXF0`FA`po462LeI?Fd{}P76N0x< zz(sDONcnf1F|*PpNrpREyXM0al(jY+`Ak6y3qEFg_aIZ7A_#uW5xIO?`O6&sxg6Q+ zD!zv%Y=rCscHw%dT{t@VGB8PF;JlcCu3u3gb__mGA#3J-2Qlc_>9y@j$}_D7|4=&| zOut$#j}ki~e69HbA($pCX?omWX!0heraJWsPYPZFr)yZ%#SYR1{L!P(St#4)Dgep^1yJP{NW zbP;rt6eLi8W9m7uXGnJToI&lIyy-q*`RT0z2+pF0LkA!dE?S-Hrub=QEhl}?OQ>tI zSChv>XK`_{2fPcY0296xR!q~_MfRzukrLPP2k&5TNU@Jgba@rKoI8B#s$_&{;mBYoJng8dq z0#FxT34anqJS8D;t`cz=+T}2XGtdfz5%RPyX1*ooOD7+JotNOh~AFW=jbO z{o{k9l!H#4=JWuu)CJSkKcL&%e_{8Z9@ha91c0z=M^UI5sJ}3v_ou>v##sZmH2vsX zV8|Zg!otE_0Hbb0B47LW>2N~dcMnbg6Mq^k+pmuL9X09HA@^t!ModD80%|C?zP{eB zrMY>cTk`_HE|6Mn7QpelGXYHoriJ}IHeKJ&fUR8s8zs~=<0hOen;XwHtuEdq6m<7( zEhAWAxigG+&GCBY+CsSE(+%8bBddjSDPLFd|^ zdE(QfnJaq_l$;|Y0bnczDJr_>t6PBqIe@nq+yVBY|K3bl7uZ+jwKIBrJ_*<2Z-jw7 zNv#~4)AQEx$fHl$*bTxGyYv0q{bMB=@9qPvPukjl`9mW{cD|ARZjRH&Q_lQ5Lt%H{ zF7E=v8kg?QQyaqv@{fGG3PuAG0?=SzVS{`g{rqQTurFIA#&~H<+xK?KwPqdghUOiv z>0Yl}cqJenX09VOJ{@YYcLh^_RX$TIsCa4S$Ha`o6>e|UZ|Uu_jjdJn$~AIO8C~ez zx2)z*z5_9JivfFb!Ovt3= z!+7woEC8N>3INKiX49o?{f9Oj_YrJcE{Wo2`?vN3$zGO)7TX8TxqN{Bi9uMM$?R$W zq?uuPJ@&3P=~wT9Dv)P&7|}^+~r*->1}BUgJA=|aRAaB^p|7BFW%tunPW8{XC$Ja z(58;7%Y8OJ66Hom?=}iJ4ctih3aDn34pA7Fw&`B&&;&_E2y}obDF;;GDQDGle>t`) z5eJAU+>Os$`wH-XuV=y&V8bFrO^`#8R`$bRrUFz*_MNu*_@-FEJdGg@`lG9VAP<&G zxe;tC9NZve+q-Zc2?DRJ8ma1E_A=;#Lqbx4!3b{o-QC;ASdug^aM(nFrJ+T%0{>o` z)H^=!l-cuZ*-hALP*YPg18lQ)%^g>*7}(*BRtZH(%x2yo|4M?&)Zw=c?m2=xYXTZT zFl{}4E+K|5z6E?WR?X2@Lp%67ehnIfPvvW*28X@wW-rQ>;NZ7>ueeuESOgXSXFlHa zF9UjwJKFzUh8a6nLNS{sAaSfTO#3FL0c=TH;A@HQ|1KKF(*ZtJy6G5ctJh0{6bXp; z2Eb1k+9rTRGJYOl%zVU%qiyi@z#KRu0TrHD%fpiQp!>OgfHyKS3f+^KsPfZQ7z;K6 zzl2v6m$xElN&Bd!MN4w<8tM}NKSm>$H(>jbkbC5!g>?We$+jX+Lr(O5T-dXa2%&N=F_I0uc-Z^5Gefomq{rmjZw z*CaAW+eS-Ch)OgGgJyJZu|e*0^Ux)IO~Z|L7S{%vHy0GHJ9=RX<7X^sSB^nfVPiB? z+E5RCn4M@IQQW0oW4pzKY+)q^SLm`4KSMF!R>+YEP#4GF`r(uW&C$qI6l-|x-y_z#SoIw4Xm%o3>$mH-1HxUAEjSle58u!25I02jwqzhlVDAgp?&v_7!4&n^NG@VO zbR+-?z!gh~D%aSJXXd~f2OJ__CR9s8z4%-s@1IwpT;-Z@=(pT7P8(}mBUs_)Sx?w+ zBQ3s;v@~?V0j0#T4G7b;9K$-bc!Dl+C(S-BJx~dsL$eSm+01zZ4gQra^~zWq%x26j zNzCS*dAZwOvEC3Dz}Wc69O~qJ(nA`>=oh|#Z3bZ&4j7bX&p@OerC*vszD2=A5Di=JhKa%eR8h(0K3w9`Znatr#0&^3vYy7BJbLg$jg z7>9`OH}lUt9J48@+w8au;{Z;q0Z5KDl0B4z0R02s7bGMyO9HrJXq!uDWt|Gfdu~`} zOw&RyAG3ojyQ6o~(;>A)i6+UHgQB7Kxfwr07e?T$CnhE`f>TIB;(t~R`~<=q;3tWr z6###PfW!9x|MCA60v0&Y_-znEH4+_ax&~azE!Sri6N(`1b7W{EDG^Zr9(GR?Iv?_{ zMIuL~(Rgqh$7{?5WKVdmm1OufxVt2EVU~(JX&mGEt@w)c&}~&wV)w_?F>%tBmlqtA ze8w6V$qUCII|YwteMz02t<}H^D9HTq%NsTPpzMUxoLq@p$5z*WhOlK_+3yJlOn1YvnToW zmD#QU1mKlpmG#?Ta+cEl*{?-2K)%Wta#r}QuGD=ItZ6SZ^o2@28}lKNgYqk&DWK4T z|7guZ(G^M|3&RxL-ZGe&0LfKLORG|r`?xefB-(h&%*?ejPac3rMB}ELkDg?pn|Bz+ z7w-#x?FvG5^N`~0Z^fRyW$Dw(7)y_+L$D;uVH>lCo_KKNy9EaYz16+d`EUS4W+-45 zjh(|)w;p*~@(@2Sw{A`3NtYnbortZ=CQT`@s{Pb-42t&>Zo!{yO8xieK8<} zna$!I61(5W#KFPAugud@l;{Hdv;irz?0dH5or=s>sx`b_DS}%TFD_e$PIu#s6K-hu zkJNfR1Gr+na|Q_S1%Ra#F#GNBwcp#I-E-n}VY;-r<2=DFH(WOecixg902>0%-ZkX8lc+k z>FdBCt0DnFY5?0FXkKImHk@`4$ll*z%P=Wi1{l7fcOd{d3W&Q!YY=|?GdDLfKU-pJTSpbFsk48(fe{or(?Y}&hi$|gfTA!V(IhYQgcnhp5S0~g* z^JDkcen6)zbg=+x;? zv?OiPgVx7387?u;Z*l@fTLQVriukjTG)>m^P;X9>H(K7oDu^EY(?0y@d2S&6f8slI za1-MSiEYzCGBjbwiTsFm7_{`TP6iUnxbhSXvm*(g4>MGT-sBQ=tU|Y~A(?Ed3N!@& z7qZ2IjHD;hBlhp4Tm!qsKMz7dq6=<%5MkVOSbx&y&rdaNydch=8r>>KI;Qh@5z)j& zBDH?o_Q2-_Ir&})_;{ZiFb;7nLm@OPR$Cha(2{TCAs=>;hbIn5R<zB@Kh?UNd1#5;{ za>eNRa&EOj2fRdm1RKqY8+1tjCW6i1n|7*mhY7REN_v9wfjeu@MI=2n#-NMnR8;h&T2(8$lkAq#_KV2XSYz4;}_^$V-huYSkP>5B0o4+8vFZLG3fn`IO z*_pZj!53eGO)pDduq@&sFD#0N_;YDP1q%J~QoN1@w`s5AxJ7l@CCS|NKd7<#m zgNwjA!oL20`051lvn83k&k)8e*R+q!?HN9wIZc~$DbhRuK~f6dvV@>eT9P_Cl`Lff zWc=L--3Og)I(vkCL_1oEYL_ z_->aYFY9RF=hm^Yr$Paf6eqXJ)=l5?=r!XQimhj5ot9r%N>;Z0nuFQ=VbE(4PL? zD;I8!q;%IJnX^uMoEmsMe8=p^ zF%ZMIPnUj|Bm9`0Mf{9A_EWGs>yF^yV}4Vi!EV{_Hx)?yNz@_c5@n}m>UmlG?3Nko z3k0GGUM-6r8{R)2!gbHrEzOp228vv#8CZXG#)HxC!6KT)we+v$&3f2MTqlP-I*;D5 zYCrv89SN3U=amdT{}K*#XBgYOhBl^o=^b0t5uL?+ady7V0RNex%|+{~J5X)YD??HE zN%3X42(DIZpcc4P&)JHunzd}0^g9wypcBEPGTPp$S=36bh)*3GWs~cO@q#_9iuTOW ze2I1Y;D^`CGXf&Zyh9)3ju-;u~Ru>f|+p^rb>u^GkCSGv%)HvL(Sb7i9? z2jGK-lISZ8PaJB^X&sB7_)2(;1{5$5OMf|2!N>okA&i~{)A&^^4!sy5+4b8HUtMG9 zxJ3U(hquwGKc=Uw2s}CNB0it>bXRzp?=C6+$MO|nrU2oUGjDEpw9aD1Qe=jfMv z;w8{Bs1e8hQ)mOpMTEyN)KC>d)u^f}^AN;$qO*s8w;{~ZRH_@SKX%>85tvJbvC{jb z)#4XNy<$sdV$SM$*B6xUtOtPiRT)~^4hmz{hem{G_SF4gemZa1H8?f$EkjQ@-&7EH z8_u)gc{Q-NS^5m8CcX5=F3-q2^G@AyoKQcK{N;v++>6KTF}tTzEaw0f(JKUxbJ$6TG4dDor(weX~;#I0|&DfZ%-(e8l9(o z<741Z{OVIDjrwTY@kZ{(f=%+%ReP`ovaSwF7B0I2SmhI{JdH)y18(d}PQ}O6`j;2{ zCElucdR$BMMn|#LGT30MfrTQ6U%wzX=t)e$%QGCj;9iDZ^!$3CSdHFxB-Z`f z3L(OEobIYNvS=9fD|oewd$>)NgzU?;ht8DKmJrSoPfZ9EHnZ_f_{AE%=BO}YaeZ0x zY8Xi8=IQw)aAArOkwDD*J9w)1fT+6BT%SkZHb{AOfd<*LY~Ze3eQP%y%?nLttP89# zuk1@jJ91?CMphN5mJBkF_q|%2gymepON>4;ZMN&jxC-}e5>M36sB717taNKd9_i2@ zwmL_eukS9Qj4w-yBC%|6HrS()TqWXS8QmV;^&i1!{IV8XGQ=jti893BL?6(Z;MI}{ zF{GYy`;?uqhQL3aft`Zo(U`XH2i#L(qm+$?M?jbQ)c=$FUVKmCYT=Utf1;aro<)pa z%e`ZLSBRC~lj5_YcSP4$yH##G^*`A#oOI`iRdv?qJTj%ve=;g5nm3}I?-T@M+hMGB z@5Aii<|aEDD~8(^<%QLLd)nyq9lk@<>%Ow1;bSYZbmzIzT*YlPE#sS|tpm%FgQuqA zt|iyGwZ+Zo(vJb|J6PiqE2%23}yN%!fDM%*%gg*xyDJ{Kc$}*k=q&o8wE%y}qmtYoJM& zd{$lH^yz4SSXQ?9rjL)OVHjy^wtw_W^V2N@X9j2EDTO;TUJCRv%tAE}n*}*Il!{#n zifcBD1nB0f#8*5<+ZobonH1lLP`2H-(3&>*r>$H^=JC2h;55GWNkKFs`sjXjUGdo| zn9nV9wDjY^uC&^Uf=6m44b26WrkdCLul$0BF@G(etQ(-a)<5`u-OIBuONKe`PQ>4H zN4zOr%p1xj(0Og7Ix2$)PgGU#pFY#&>*clU258d@u&;N_X|8$(C%|LPcMFyVclrcf zi~iUU^@(9qot&{BZCg(irw(iMZEB;nfC)}|^ncESc%gZ;<_V1=v%F4f?!b=;E9_~r zPojmIewzns{zs?Fv0yU`!{EKnfg=;x@;Vgt&GVrlZl0g|5L2s^H)pt`gXJ=ziV)R3 zH`IzWkGnW}EMG!1s4=*G^ib{C=XVA~5($FCD8D zIq@RpqueJpDA(KH_tcx>%*LaA?_RSM5c1g-nt>fci??0BEm5jI_Ijx<_dj;U0<-Q& zk6d>zrm-tAj~JF}_AlI`8#OnLxZeLAG?cqT9DVgeU}yjI6c4bl5k@}G-FlvA+fyE{ zqm|!2h0^7E{w4D%2lIfJd^?hb>iuBx>lP|b{Q|@`;>V4odfq3^`~C_mr_rFfFgQ-K(}{e(Gzdig4ELX*-Idq+eT2Gi+MxgUSqhW(Fx)n5|GL=r^W`~2 zIkjh>!?pAtnCUM^;HzKbO#F$x-}8K%1Ft(d^a-zPQ0L)7**K0@li$_Yux1o`2BIMn z^l=Cy_HW1wrC*$Q-7HsF#^d64E4q}=b?0^< zdValsW}v4t6(umFG48q>JarvCUl$(3t(aeL+<$7SHhxQ#G+G2z$}IB&wHcdhj!ycN z_+gOfHRV3#MvNg!)>oDc2s4$9ns)Eb8{b9=m~7NFi+Z{4Cj2@!6PaE6_r{c~Gn+G? zAKXvmP3xkS$uk8g(Ce@O#IHXLQ#Uc(vPqHrTZ++3k^1lA`Lq z+RHsND~lddwNbA%krNkSAlF4V6vX|n0MG(2{Q;GCIH^e+Uj|OJ{d{@$a7jDZzN;bL z@Y2RjlD4Nx9B(hrz0weC4$yL>sN8$HR`v{VZi)F-;CbN9q{#N7p6RrRh=}D?*Cj=^ zr3e;4cqrMt5>Fz=GTg61FHZp*2>@Zx3v8j)hH2E z@AB8S=Tl8Z)eY@Qh>E*`&44$PBHIgrpEkt1-1ck0f7W6xDE(_?WRrI~9XQSQY)Mmq zA4!^CJBYR`r&=Q-A_hv=B}EM;0=EE2THp5L^$L~s#DA13;kp-? zY5Soii1}Ak3!HyiuJ;F4r&?e=4wwtfw>_<&@h1X10JDIVsn$R(vVC=}-o?OCwqI%y zXC+{&?SmT1)&~v+dJ?h6ZC~GTe?MR?+f(|}_lSsycZ04U4v>;C+$!l0rlvaR^T4 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + To be placed: + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + From 549ae07acdab68fb018a99879926f067d5aa0116 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 26 Sep 2024 21:07:02 +0200 Subject: [PATCH 4/4] "generalise" bumping scripts --- scripts/update_mathlib.bat | 6 +++--- scripts/update_mathlib.sh | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/scripts/update_mathlib.bat b/scripts/update_mathlib.bat index 48cd7350..83c2f97f 100644 --- a/scripts/update_mathlib.bat +++ b/scripts/update_mathlib.bat @@ -5,8 +5,8 @@ rem Download the latest lean-toolchain file from the Mathlib4 repository curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain rem Update the Mathlib dependencies and ensure doc-gen is also updated -rem The `-Kenv=dev` flag ensures that the development environment is updated, including doc-gen -lake -Kenv=dev update +rem The `-R -Kenv=dev` flag ensures that the development environment is updated, including doc-gen +lake -R -Kenv=dev update rem Retrieve and cache the latest Mathlib dependencies -lake exe cache get \ No newline at end of file +lake exe cache get diff --git a/scripts/update_mathlib.sh b/scripts/update_mathlib.sh index f24c177c..ee844740 100644 --- a/scripts/update_mathlib.sh +++ b/scripts/update_mathlib.sh @@ -4,8 +4,8 @@ curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain # Update the Mathlib dependencies and ensure doc-gen is also updated -# The `-Kenv=dev` flag ensures that the development environment is updated, including doc-gen -lake -Kenv=dev update +# The `-R -Kenv=dev` flag ensures that the development environment is updated, including doc-gen +lake -R -Kenv=dev update # Retrieve and cache the latest Mathlib dependencies -lake exe cache get \ No newline at end of file +lake exe cache get