From 17dcc467a3032359e0244fc2c857b4840d2c86a4 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 4 Dec 2023 14:52:59 -0800 Subject: [PATCH] Rename DafnyStdLibs -> Std, make collections modules not plural --- Source/DafnyStandardLibraries/CONTRIBUTING.md | 2 +- .../DafnyStandardLibraries-arithmetic.doo | Bin 17788 -> 17773 bytes .../binaries/DafnyStandardLibraries-cs.doo | Bin 743 -> 736 bytes .../binaries/DafnyStandardLibraries-go.doo | Bin 769 -> 762 bytes .../binaries/DafnyStandardLibraries-java.doo | Bin 743 -> 736 bytes .../binaries/DafnyStandardLibraries-js.doo | Bin 743 -> 736 bytes .../DafnyStandardLibraries-notarget.doo | Bin 718 -> 711 bytes .../binaries/DafnyStandardLibraries-py.doo | Bin 737 -> 732 bytes .../binaries/DafnyStandardLibraries.doo | Bin 20244 -> 20219 bytes .../Arithmetic/ArithmeticExamples.dfy | 8 ++-- .../examples/Arithmetic/ArithmeticTests.dfy | 14 +++--- .../examples/Base64Examples.dfy | 6 +-- .../examples/BoundedIntExamples.dfy | 4 +- .../examples/CollectionsExamples.dfy | 22 ++++----- .../examples/DynamicArrayExamples.dfy | 4 +- .../examples/FileIO/ReadBytesFromFile.dfy | 2 +- .../examples/FileIO/WriteBytesToFile.dfy | 2 +- .../examples/FunctionsExamples.dfy | 2 +- .../examples/Helpers.dfy | 2 +- .../examples/RelationExamples.dfy | 2 +- .../examples/StringsExamples.dfy | 4 +- .../examples/UnicodeExamples.dfy | 30 ++++++------- .../examples/WrappersExamples.dfy | 2 +- .../Arithmetic/DivMod.dfy | 2 +- .../Arithmetic/Internal/DivInternals.dfy | 2 +- .../Arithmetic/Internal/GeneralInternals.dfy | 2 +- .../Arithmetic/Internal/ModInternals.dfy | 2 +- .../Arithmetic/Internal/MulInternals.dfy | 2 +- .../Arithmetic/LittleEndianNat.dfy | 4 +- .../Arithmetic/Logarithm.dfy | 2 +- .../Arithmetic/Mul.dfy | 2 +- .../Arithmetic/Power.dfy | 2 +- .../Arithmetic/Power2.dfy | 2 +- .../DisableNonLinearArithmetic/Strings.dfy | 2 +- .../DisableNonLinearArithmetic/dfyconfig.toml | 2 +- .../Internals/DivInternalsNonlinear.dfy | 2 +- .../Internals/ModInternalsNonlinear.dfy | 2 +- .../Internals/MulInternalsNonlinear.dfy | 2 +- .../EnableNonLinearArithmetic/Base64.dfy | 2 +- .../EnableNonLinearArithmetic/BoundedInts.dfy | 2 +- .../Collections/{Arrays.dfy => Array.dfy} | 4 +- .../Collections/Collections.dfy | 2 +- .../Collections/{Imaps.dfy => Imap.dfy} | 2 +- .../Collections/{Isets.dfy => Iset.dfy} | 2 +- .../Collections/{Maps.dfy => Map.dfy} | 2 +- .../Collections/{Seqs.dfy => Seq.dfy} | 2 +- .../Collections/Sets.dfy | 2 +- .../DynamicArray.dfy | 2 +- .../EnableNonLinearArithmetic/Functions.dfy | 2 +- .../EnableNonLinearArithmetic/Math.dfy | 2 +- .../EnableNonLinearArithmetic/Relations.dfy | 2 +- .../Unicode/Unicode.dfy | 2 +- .../Unicode/UnicodeBase.dfy | 2 +- .../Unicode/UnicodeEncodingForm.dfy | 42 +++++++++--------- .../Unicode/UnicodeStrings.dfy | 8 ++-- .../Unicode/UnicodeStringsWithUnicodeChar.dfy | 18 ++++---- .../Unicode/Utf16EncodingForm.dfy | 2 +- .../Unicode/Utf8EncodingForm.dfy | 2 +- .../Unicode/Utf8EncodingScheme.dfy | 14 +++--- .../EnableNonLinearArithmetic/Wrappers.dfy | 2 +- .../FileIO-notarget-java-cs-js-go-py.dfy | 2 +- .../FileIOInternalExterns-go.dfy | 4 +- .../FileIOInternalExterns-java-cs-js.dfy | 6 +-- .../FileIOInternalExterns-notarget.dfy | 2 +- .../FileIOInternalExterns-py.dfy | 4 +- .../complex/Inputs/randomCSharp.dfy | 2 +- .../complex/Inputs/randomJava.dfy | 2 +- .../replaceables/complex/Inputs/wrappers.dfy | 2 +- .../LitTest/git-issues/git-issue-1514.dfy | 2 +- .../LitTest/git-issues/git-issue-1514b.dfy | 2 +- .../LitTest/git-issues/git-issue-1514c.dfy | 2 +- .../LitTest/git-issues/git-issue1495.dfy | 2 +- .../metatests/StdLibsOffByDefaultInTests.dfy | 2 +- .../LitTest/stdlibs/StandardLibraries.dfy | 2 +- .../stdlibs/StandardLibraries_Errors.dfy | 2 +- .../StandardLibraries_TargetSpecific.dfy | 2 +- 76 files changed, 149 insertions(+), 149 deletions(-) rename Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/{Arrays.dfy => Array.dfy} (94%) rename Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/{Imaps.dfy => Imap.dfy} (98%) rename Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/{Isets.dfy => Iset.dfy} (97%) rename Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/{Maps.dfy => Map.dfy} (99%) rename Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/{Seqs.dfy => Seq.dfy} (99%) diff --git a/Source/DafnyStandardLibraries/CONTRIBUTING.md b/Source/DafnyStandardLibraries/CONTRIBUTING.md index 0cebdd373d3..08658e47249 100644 --- a/Source/DafnyStandardLibraries/CONTRIBUTING.md +++ b/Source/DafnyStandardLibraries/CONTRIBUTING.md @@ -142,7 +142,7 @@ There are a couple of things to watch out for when importing libraries from the and one under `src/dafny`. The latter is a copy refactored to nest all modules under a top-level `Dafny` module to reduce the risk of naming conflicts. This is a great idea, but it turns out that using "Dafny" conflicts with some Dafny runtime symbols, - so these libraries use `DafnyStdLib` instead. You will probably find you have to adjust + so these libraries use `Std` instead. You will probably find you have to adjust documentation examples accordingly. When the latter copy exists, prefer to use it along with its the Markdown documentation, diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo index c3e170af1ba899a1a29df95552376d40971deedc..ee7d269460bdddf32b9051ae7362c2b80e828b3b 100644 GIT binary patch delta 17353 zcmV(vK>+zlM>YrcCCdIEeisHPQPKU*F{$KX=*@FG&bv0hi7xm9oXZ>|iH_L7@ z5&s^r=0!2DKCS9`wJ3VUaWN5(s%Ej`PjFw>?Vvb0Db~eZ(e78({pV_U&YQlPEjkBB z&O_T@y)u+Flht@x&zdKz<*YO5e-;e>syI2tomLv@iX#;uu5TnpDF7azft=0e!}Ie3 z55M^J>*c)u@S&Q^Azc?=e_c$9Q^trBmySIRo~GkUVihfNnXf4*f}-v!esPYGT>ED8 zraC|Ckh(A_zBo}7X?i9cGbf>MhR?CSe169T7!uPDXT5A}J&mmw!X}`Fe^7lhT-4)* z(s!&2Yk^FNm?K$hB(TNZqA!>o>bTY&EidXb-M|%$V#``dqd@#vCuAhX5z%O%#9}l; ziPJ+Qx{Fb(?&SD&pKh^nx@}aqQ;zjde`4=X0i!nJ`JO->OR9eL&54=Oa=xk@D+;qB zC~r@GN|%77JWJka5**4Me@s0=KOBgUj(L)23+_%hcRZbWw)kN_spi$>o6UDsGn>}U za5XkMlS>K?X3B^nlEBrl6el&H!AAc*u+%9f2@s}Dj6LE?+D>t#d~`a zISzTb(6k}IuMqeZCT_)_$Ib2KtocVZpT*}%A!6&Xp%&?$R zR1V#3WqJk1q75Gp0gDi{cI9F?mz;J&8jLKdTU-W06m2%_H^mVL%1IPL%y0+ z<9Rh)@Rz&CFGS2CTMQSAYQEI0TZLkdm6U;f;0Hdjhy+JQK&g(4OCmNvFk`GNdCotR?Oo(v>oIoEA_NJU3|tAtn_M(-jSn zm{A!^S&ao^PV26pZqH3vvQ~=?HW~%4~A{G5;a_t^~FUhwriB>=e$6 z(JEO9XM2jqMoN4FBn>(fBDO5@r5l$}(o5Epy7};CHC=Rue~PRTBClJ#j<4a&qu1O? z42zqL+QVWb{w<5nkpFSO|8j!-+eJsestNW zo@04(537A#e<6Swkfe3Pgc*ww(NjuqgsgYam(M?%tNg(@#=X_Bd@lfuxGOY~4J$5w z8~i7HxEBWb*&DOiun~D~6m8u$U(JO4HjZnz_t0oraH6Telt+9t>>gTg(TfSV)JoXp ztMk?3ho*G~tJB2o}RPD|`tFxn8%e}(9QrE`8Ksf^8#F3%&t2nlGm zCI#@KZnly@iRme~mVqW<3n7$H3T03X8KkxmL=>Da3d`WQEJQklwWm{gz5oKLCS?6M zHbYsz4B=>s_Th&jlq6hGC`2^r4a9KE#mog#-U4|omL$GN{H5`wT)e=Q4?R2B<==Y4 zr--#!fAPo_X@~uB$d-i&UO3EGL)me8#}}4nc_#;~{l8t<5yML@>>N;pFcHwmk}hu* z_nlr=?Rmkr{{@<%^j~r<2KbzuWnRvjx)IG;Op$idQZhIQ<9~)^gDBp6Bu0?G zT_lD8`7(0&9+#6ykn#l?qk*lbyTw%e>$}2Yf9i{8>WJrNG1aMmNfZNYwwWv@hJ>Db z7|kCivtOF+6PTQ;q{|kK*mA>lk_$H8XV4Q^ea|s~quYMR1PbV*!SVk*XAQV6buWw$9A;Y~XB#*Vrm5js* z+IiC0J5aKU;|EFL4BV^v?1HIHT{(Pm_35T%wB-wP3{CZ6$eGendEJcTL)r)#EIj=e@fgd(Y-@irHD%v~m5ORt^bfFz}Lxd31 zs1uqRH!in7TY2yNjR}m{nTfX}!Ck)CX)hV-zOJUjx?zFwUoV)>?OWFYrW&KR+}aMQi+TrX$g5vw~!P;ma3KjMS2PH z!_}ByP$fx0XpV#;oQULt{O$X(THQ{l)osWW$0_R^3)LcIeV4sb`AYsrM>MqCbvbLt zpNI3}b@8LQ z4AfYF3N+%VsD@n3AElV@5@IIxAGR`!3I=4zJvpV3+m9dA0bTe_>NEe(aPV<*IZ{ln}(V>Kc-uXgDm&k76h})cko?FP1+r z-Em4wBnYVEE-HZTPZo>WxR&d2KJ*+k9f_w6qQ5r7`R1iq_|KZo$F3qZ zf~W&AZ9k@rA$2V4!gzH1ve=!`!4yHJZoQ6EX&gd~ri8D>Mo0J=e?R4-9Rs!-14g+V zM3WxX>#%t~Td@C-WtpJ6>syMVgZ#vS-yo%;V`*|9{j?d^84bD20Uhu$*oRsKo~Hy! zKv<4tJ)M!Yu4;j=O4lW}$r}20vu=SSKsc}J&nLol#i&lpL^)~*C} zIKYE|-6Bd7v14eWe*|$`ph{UkX7XAF=)?F^&1X&hgsF}g*>1=bTg?fJP|e|figCibq_rZ^FQ;_?M& zS4X|hwmdSSE|6XV%!fMj8wQ=}YC0}#X}03eo8nJ{;xw=en6*y=H;BY}vYTiFgQ(4L z>FRoHa7fMJT#{q^iRUh*7t2D+1@8nBpl5JUwuUFy40fvL0R$PPCOnO<>`53&yFC)W z#wQ5gaUPT}e@JeGJZmPbOWk}}Fc8#KH8T(}_|H?s+*gqqlgyrl06<_zWKM#x15zNX0>??(RWvawi2rHQr4D+UK zAw1Bop`5HoaQ2e*;2C@qln3|~C*Z0T9!Cc~jE?5Tf0U>Tk2_Er=B{2wfAS+)4$gx$v@qJqFKsHrM2xZ4DFQYc zTL5*}HLyv|JsTRD{abOaZ!XXEdA5>Ol`vFQ2`fW_3UdvLl|?}pDd^#+quY5%+}>bt ze~4@OV>DoH6fnV!ToOdzu7rE-KkvEEB^6ys8#~ys9AWBk8P?

_1jf^Tr`I3upq62nEf8o?~iSpW8nT-e)3(%8veoASQYcMJ;)9y&) zL@fmZIuxR-7plkc`)pZ|vv!27Plyx5wmHb?fk?_C>-ICV;7J+y3ANV6A{mM4Q?J}p zBC$6KLj|f*?X}1dO;n3-GyxP{aiqv*v@jK*P(me@_$V zAl)-H8&2c2&_`&}$0MoJk#KWX)c16zHs?pj3*xw9DQ?|aqb%BnJDK&7pminhtGX%j zoQ1vc>{8Vt2M<+7IF_H5#jNy?TMDi@r!HlIxn(MO1T!x?>!81if_F5~MHEv&LZ?K| zb{bFHs_q+cp+oh&@{+Zow3+KRe}>YQ+>F>zWOdl9aZ1<5HZw!(+DPTBcy6&<)TVN_ z=Ira#Oy7pQ0AXa6%pliq?|LX)=Vho!F)BZE>m?urS!yt5LK(?GQ8N+KKX$b&fa8h+ z}-{aJnpaQJ}E?d^Yt-YtLs;p2(7XH|6nlXG_(IX-lwNh7W~61OAigzB-$e)BV}H&SWF z=w6Hmz17}~>K)sm(FjVse}$qS+g+QTGxiu$CxU7Zdk_++uF{I4X}=c}DY&2p3^YSB z`KT?SZpUpluZ-r|y?E;8RGcMF5XQ~qs7><|F=lEveXA0UT5HS7pp^J%SR{7r5&@!t-Mnk!p2VWoTSH@4z{7pnIoXHPY083e~q&V2&UA;F!k;! z#(nv{7P`(_UX5XI`&8G-_V_0Vnxf=W-Bex}>s_CVfZCHgvb!EEngj}hkfXpmju^kU zP(r2ORIh9EOTOhonnr*=neZz0m$TW0pf3W9-y*`fb2AN;L8NYtfB+@D{eZzfL|yo+ zL^H*D=-+lyxHklEe=ovvD-n9V5ZB8zx8JNrEks!UD~K@1DQtE2^``d?3|GDr<14&x zU{D^Q&F3!SsNA)buPTY!UCe5VF;kZzLVSWDQ^OGP%x*dcc8gEXNubdtCXEClb}sPdnh|1H5fAba{Uf17D>48$2W_%Cb8bYonCm(LdZixIJ_ z$WGwHtw>6n$N*9h&fBFiEQDkIui&fWMi1xbOb=Sv)chLNe-ml zTyop>-L6zzW+$b?qjPs(H6|h7opq-A0`RG<7Q9J#?6_m|iAe9-dW;_t9xh574UqPA z0YJpeLGUvv1Rh`SD1>r%Dfm?EOA1lqT8SY5$(IAgf6{zcrRyV|d`G@T+%ARzLQ!U5 zDBOd{3=HKOu^evW<8&>Zz`XJ?C%s)t-ZUp*u@WA$Z-*g{L=#LYn+&r#=ooG3YnELu z=R?6}6Pqj&7s`-@YzrN7y4y+e8wv|uw z2_KWxf5$PqrDP7DvN=WCzZD(B8(-PN92Hqtk+ylAzS@}FhuPW^_c*rl#+IJ8^(R=E z8nydyH4CEUbK(>8uxfB12^gUt3WFG0}f658$pgK?^Yb{&@DmJ(D# zNs1As6?d|_(x-iXdw2WMHsZB7xdwic{yk5SaHSepRtNG@=Ov7Cp ze=skr5A6Ti9tqH)t-QjZ&u{w0DyFi19eKm3zG2R6vB2yh5w-LGnbRnuE>HlfeL$va zLgF(@Etq=N=}Dd|A=f|^pDmtO{OhE(tOl@u@(yR6T0^MC-S_fo07~60dH{;}(}M!* zB7)hsGayLHOp$Px^|X3kPwS;xu+@y7e+SorGA47k5EgW|_@w@wQ-TNA_=L{8fy6SC z$tO{ue^|_swtOm1;AheFrSbP?!Bc zvkWJ@Xs7fG|9qXuN<-cYowGdW4G31ZB}jcw?2|n7=^eqtuO)fc=5pH<$&Q1Ke-Q6D z!ib`an-!U`=ZU?-*+LY<#MAAeTPbi{M(mdbKW3XuGHSxM%B+JZ3><8q#_` zBdUxoLd)SqRJA%+aoF?fZ0p!q(sEk{fO?ABq~hX`v)GujV+nNyp{~LSLo}2fqH04t zxgi-H_9eFEfOo zN@cbXY?xf4E4_mpq5Lv$1m=;)2}Kbar`M=Z2dl+DQ~ykrGoM`sCo9on16rg8-1gE= zLhDnb0cAu?1w#xHzAc+Ee|a=srO`UplR*HvGw(sZOgchw_#A#-_G2v9*Y`6!+^Rpi z>s*oL{ODQLL@x(B@@9Ka!}O^=`@KPMjlK6JNs~@pgS1ZGoqojCU#+?e@;wlCWQwwn znmYA(xAT2I{EmmfKW>LO7Q&xCYbO~V1>s-tdsh@2ctonK6(xp_e=k@H!ofj|6!!$< zo7E_IFSMsd;=^<#YY|Q;4D&ej3E2pL$wFTXo4%#ayw0-iuy@7A?p&brQMk-LC@f)e z&=a|D;Epp4f(F!w5JY`NCh1oWV8_KKhvkNsQP)JCXUO9~dpZN$@n;0<+Zi#*BPlPy zN7?X(7ZC~%{YN8je-aon((qG3v3SglW~f(cZmnL6M1=>zY&Od}f>>iSVFfV=#Xj6+u@xjwbcSRE`e#Bg&fm0t-SV@@ak zhuxIOIh9?P#$YfT`)nXKCUiB(ZGI1&TA_i{z1kc31{An`f71i)&@Bft4B<+eW#&k( z9N>;G!$S%=Sjyx{|LRbaKpq(*5lbt7VehDkokDGrk%g7VHjRlK`LU&iEF$5wXtG zge2P%y+rC*@8Vw~uQ?Cq2I5(M1qfTdt3Z-M7h6r%*8CxE*m4gueU!wl*adH@LfD|*XGI$p5= zMJ3M>czhXMNh7Z0MV}iFdk0EZar__&Ji3_le5t$6f5i8tZ{*j*Ha>(*rNgco(kM#M z02Jj4v2%7Lk*nm}EU>|(C9c7w8pQ6!aVJD)5;JgObCCy!o{zHm65xjWF#+B?W|qEx z%X82>eQU`KW{b(Og@bPQ5vKfUFN*{}vILVGJr~x~iy2c7rprw=Da5Ua%WB>X&llh= zfBf=!e{q7|GrK;on`$`s!SHj&1eh1%lj#f$d>;eDZO8{>-}(>LMy2h>205KgR_9gm zW;wa@WL__SoL0+vdTTG2L6CwYAa^!PD4d!jTc}w%upI`Hf5(2zl9C;!(POx zBW$3*IA)-Z^$m-Se{(?ykdS0^V8DUDb#-CGBZ6FDr30+=fRzFm3>sC=pmCOCnw#GG ze}-||jVQm_ys6I5Oj}IgmCF>bE{}1~cT!~R(ztHQ-Fww#xltvMc9hf4-OMps$x}b>u*4(Ua9WqDUOG)gfe|Mhl&- zMc}0Hx{GlD+I`=B3GKM-6IPZ|peu33rDJ~k*QEh-&w09p4Bi~0=&a3fo!h-kVg7$jUdI(MjlSLa6 zXU6ba{X`3XrLSR+c=VG|S#MDx-gjh!Hl0cuPnp6~5_sHB*ZJb>$?M@2gT-Hx-ImAy zDcsW0fT>3QUa)V_Y3xBD_$?i~pe1wV@tGpWN&Tji#?~IHjCrV%@H8dzP#&rAPUzg$ zlfD}+1-Ea#4^NZv8yFe$r8U&4gT0(lZ4zfxd7Q-;dElI?engyAlOh}{e_z5wim3to zp_V(TB`s!wg8%qKWy2~#;WI*w9!IE1L23(uR!Cdf}wy9D_09}r3GgL&WJUt*}%)kGg=y% zkXOn0(#gh)1}H)4@t9G>e>WGcB16}zR%<4KiL&;+JjjPMWEs%m)M!xYprVJiH(pR* zQus|aIS^)E5WPBLu0Bml%>-qZ+<|KZCmxRPxFU9ZXo^t`oue;e9MM0>_Mza{CV zB|Rf2;Oe20niUM*PUm$E0fiKcJ*1OBg{>BN%WHvZ_e^D&TZ|7!@Z}TpPrpHayga7N@>V)qYyVjEv190lj%;=XN$SVC`BqunHwvH!cBgi23BQzfC&mC#{OLQ^TBa%%}qb0jpS zBs5J*XquLgtS;Mw4c*idx+(n8ANI2k`*|U54c>$O>{~j2f7p(yFsaUGzw96%zsf>O z$_o>8B?=KJM4{OEpA8(ev{8XmYiS4VC#hc#n-3LP#p3X#RUK2RwCJW&TI6VRep%5? zr>tljK)*||Q%*hC&0sy(HaZpLb<(*|P)Pn{P4ipmdDu9aU3!tIJN;2@Tqo?cAwp5A zO&Ct=D@Ff%e>Gdy{Jw`~^17N1>t<5fZ%E_I1(~&G=E%&|fen6cE)nFy3*0%04QP%v z0%cV`*-uP-QkkkxH{9(fr^v{3(?W*%Nt4FB6F9IinQ&fz;wsgp?gtGQtE)-Nj9qN# zeUir}HJn2|oHBnnhlQoV9}cob zx8~B&F*ikpjup5mWV0Wcu8C~4Qz*@^UPk%jP1zCF`k9ADmjk7bq#IU1!al2g9p%lP z>L?Z7%T(>8Zl`w3Th>d)X-t*AU>XDEE`~srE27pkE%v}s0c6w(<(-zM+)uiZbFoG% zmDopRe`G*AylP0K9cbF+2-lz3ls1=G?{WtrkRx{zU2uRiJ={dJpIRG_#F1y^oRTe7|9v&4+LkA5ke0 zD5m!dc-#W3|LkgrWC4$>m^*HD{-Ksz6!83^vbz`XQ0F?ym2B%1qq`LUgexspPH7KS zX|Xzo2T3=<8VgZ?V%KS+4ni!>V#hr~|xix+asocA8S?@LZF~8fQ2a1vX}h@vLu#U$Ho1CQSHH z;vO8IhoKpUbj0Lx()%_|&O-8^fBU0%L7qj^5G|OPT59DCwH=()7yby#%}gga@>h$y ze{<=#TkZc_YR0y!c6!k~94*8b-3xm4{JdT+&#R}+q#iae`A6;Hn)RC}Z=QAz#5d=W zl;rc`wCD$JH2TYo!BXEaT6|qBs!zw0`a``uHNebL_iDYkN-wcBufSz?e`+TR;`(kr zyZFAIFE~~)1uH@i3-i=lmpequuU+hq=2x>{oI4_uV-Y0qp*$bzksKEKHyacK*^vY5 zN=ml5dc|OR`Y9|dBy`kF+}HydW-U|QM+KTIeTOeZFIzUTUT}DC-zgBzmI7-4*@2q! z|DoF&`Tr1MN8m+@i?A&Oe`tv3y-=%b0y=ze6fX=~`IE37+u8#kCzgtBrQ3MBGx^Ng zUKzt)NBFY9Mn%{nOVY9Ppda=`-O$v>+3EI*22biM7pv$8kTlk`D7OPPUeh2~lc z^AUWfG%xasGqOiGe=gJ5DZ)rxuT9SUEmWH|RNr#W4;znt;$3EgsR6~>dT>FVabg{w zKRvISTRelR=Qo&Jy_o&NUqO0!bHfQIQVO|C=#_K)1e8E9`hq}1Iv4^J35?i~b>HK* z0|>@vo;n0tT3R{hgLIvQ3G)|IZVPlk#%<#gpv10o!GH(?e|O@Bc?jLrD3Ch{%&O`2 z8sqP)d39E=9b@YjwOF1~Ur7+Vr(E;H2Kn~Ro%$VD68yBjbLX8KA=SBllA5ToO^ZFo zzTvSyTM5GY@9->wj9frD1wdlf+G>%g9n?v1xev)IvhUH(UE)@_-09Rg3>bb z;(_p@5rhjTp-(~PeVC-v2UsF#f}eW{&y1;g(T@f>MtR@VkwDw^@)Osz`ml)lK*h zE7w@q2WASTG{XNK7HZB^RE0ZioDLheL!Rvd(4K58aA>6VjnO}Q<&faOvB!y!BQ&tO z#U>0me+6d);gAHT)*bF_AZ>sX)h*!0QD_;JG?|E3$8Xr`@e3}@w(2i=Bntz$Kb96M z&SbKGxo7Ul#hM(*FF)4j6}r}?ZdkW^*ev}UU+k+jvgDf7me?z7fbJnJWNqk$3cGrQyDO>x(A0Sla zJe$tZWkQRe?oEjUi8<`9O_Ae5^4KV`2pafit5zOu6M-CwF+ff)Jt;1DK|poqT4O7XH`nso;Y}m ze@4{55@O~5<5^v}0)p?zL3lK^+dMXeL!>aJo?^is(9vTw-(nZ}zWDw_dpY?F8E3&l z?52M|pG_Iuj+{acczK+s??y8lZ#Vs|oEzNjbn|5ow3*JHny;zr7jOBgXi5J&&QwiK zaTl0|Yp1G}NP#yXO0^#|5_EDsyfP3Ee`J2rX?PlF_k8xj1ojOVx4kDy8G!Bp)<=S6 z3qIXhXh#n7evO#sl>`tV0GlDnXY&njBW)#QT1iW=NBe@4? zhKj9lSp1S1Xha5%7!p6@A2nkyZnRXq$)@5oNCd&f7cFIT9kjhrfCCSB!dk9On4KSw+r{%4zVemNA>Gv ziR*1PaxQ2>y1VhB{M~pu@`r4LH{(T>UNBU-%wtV{4#0^dL3v)pxvwCRQX0H~I+*pm6f9AZL%`PMy z-C8dCyWWXY-$wNeC=qJP@rn}c7ejc=gOcBuhw|tu$T4v!L;hR6{E?g#$q=;FG^y54 z=T%U3)q>T%zYxp@5;hndzX) zjy-kT5?TI=V^+KI1nVC`fA32#ghC9Vil7qSPV`IZOG+DB@G_=CJ*+|?XM~j0t`XL7 zeV~n?=c$|37xh#)NV>Y?jhC6kEbvM>n8^@cTQ_%TbJv{`g2=2TqR(X2knd^C^Z*J; zoM0u3yf0v$pWYJW>7*Q3JlmX#aB|?dX(__)54dU@j51SKTwSWJ9E84Op10=z_MLbE=v1hHzw`DTKe6G43yP3i zjFP&6guq?IF5FsS-bVCVtfum?4(nrf5D(2>EBnbH%BCIG_B|sV4409~9@?M(8mQ zc^D6bE+u=pG7#l*u6t2L?5pUEC@k~ptGCiB&^J%FK!?kqPVpyV3{ab#$(X-V_hTuh z;%4E^%G`~_@XGPh^JfA>@Uhsjzf2Z%CHc+OTgfNrrOARjf8q@nALA{9CF#ndkcBx< z^)98bdyoBH4uQ%%0kEdoy z)1b8Ph4q2Cf79e!B8}CI$|qD!$qqAWTG)GKotL5gRlAEinYi*C+gU@KG<5R)Q@C>}rO?Z6wcf_W1l^kWV z)5$K4%}gY`nKvg#;L1a074XDV(*oPM~0^{ z14-@_>(@pa#A{DjP%-4Nw3f700zN$g@sq_PNaE(&J8w@y64P*xZWyP*cMDyGKoxyC z>j4xt_)0)=pQMA1as$NC!A~lXvA_hAZbO*zKv5(rs3M5=E?}@nHn6c((XQ#@Kx|jH`baR8V5v8Q_8(@e%k;(Dt43V=zxdU&-ogVMkr) zYVOB|H#dWp@E7E0Hk)EOh zms>lE%Pw*X07#1nc<^^u}^0tuZOKx$|q+9hZOg3+jbfI2az9 z5}LL7wE+`wgimb=y=qAXIaQPN_*x6~56Dgvl;ei>qQW5!4k<99zajPQC_bpmt2%$T ze`cw&{_0m+on=daF6s_HuX0C5ZQLf(Fsxukzg#8H;pXW`LzNInp3czX#wOE0Xc33?~jDwQhOvZuH=hNUsaqXK270moeqEIKV(7r+B42XMMU(<)Q%J=^%({ zk`t!U6Y_siq>=G5ZX<6~J{rrNZ%l1!tR{d+0`}CpKDaUNBZzE}yN!3;D9@layb~VD z$3ZZmfRP$;Vu^6Rv4y|U97aDU*}d_`8c%!mO{PF6x{_jYu5sE@PJLfaKJ6hn^<#3{ zWXTCIJ!9#fC7`U`2$L|&l~4~#=p-(p{fLGzA%cJEt!xOvp%&ZuLIF2RCB>4n%h}sP zFegefy`*Hkd$6{bjlc0okRFjvY|F40mk;83QbK=ihV#u!(SFuMriakRfYs^A(qnHh>|1=No9?xMNw-498%0Lln=eQqTg3_sbl>+t-=LZYOcDoz)#A~Ak9_-*=;fNr>-2@1z#dw{~U4VXIuWos}V!x zJ?V8h-NHMZfE(cQaQu$A|1=m-9uY(H7Hfa**u0nUc%xj?7vf~tvu0V%n<1OQYPEP#qIGA(86uihK2=2WH28&SROq@jyI5NiZ5I7Nztl^UdDYSW0z5_ zW!z85*dp*{+>gq*$01bIeF2qMc)*+Xn0e7Rrhw6eSuSk(3-8NCk_vDfJ49+&5*5Wd zL9LKPWunyVQDgwV0$hslsh~z18EJpt6$*sh*N|gABP{{vkas^v0{!+9=o<-S)1Cn? zXbT8IK@Bl7yf-Wgm{0ZipUwY-UKpzXBW%^Vpvutn_%3=v4S*GFez5_tkwf)gWLj93a1HqmtTW z9vy&SZQx!WR9WZ1omIa;x63&9zyv@ZnFh8g9X;S%K{8^${&dh((pTrtA6>D^MWJ08{xs_hce7tqI3sBhx<51y+NAyD0_DkV-s&u)85O zvKp9CBjQF) zBDli&)JLot@O!Jgu2}Na=X|MUtqUx?QuP=&Kpn1KxQg!EkkSlH{CjJg7y9#64zw=l zpTe9c(bS6Ah#Chy5y8>jW0s-_265G&{$%t8p=+rOfoL+I9y<_z<Ls$B$t|wxBcZiB`mir%LbeZn>MXWt_^7E8OzL4t;9;EE$X28 zW$L+Wf`ld|@@M&X3BHnf*d9v#!p*!)0DS~N#*i5W8$O_o1hgqmPCz&>UL=UhgW30C zwxcszBCy_D*+Cz|%mOKapJV|5+shntQIzEX86=)L$_k=3o+=qct zb$R+by#BBa`D~?Ioy6(t2lhHVfa-w_gA#y2l9WN{Miwfjk&qSv-r;`%njg7OI~Ym` zmulv%MU{G-Au#wRb7#v?re3TA(ZVTq-|Sj+3NiKht-nx zw;|YC{fko_Ii-eF{-;NuBYUM%@*{N<=>dOCR_GT8>ZF=qxfnP^OT7kHtWW`v{!E8g zgy2!9wc17)#74mgU1Nuf0NkPFLxsIyCl@+mT9(wqh8E0pUE)(&m-={AK+=w-(AwqL zi^uzGzsz9^?b&t{YFFCny3y8yaE%_?u2j4DZ9*bZ_jA2qK`XwORt#o`71%)dCFg%r zmut9erz=+newE4^)Labk%D+SrW~^dFd}j^8IX!U!xgmG5!%?*T?F2UT9t8a49oSCi zu7eEDBcc4uTAY2oxf@mAubRnlS~bhzx%?C#_q7D>tR1#?1XAR@3KtHN2vYFafb4N{ zir8!;$_Q5mk!mf%4$$F(uyLY|6k2~rOuZwj;!-9nzdr*FRqeZETH#ieT>Bio7G(Nk--w~q~95?(31v+mY6 z>aFro1Y$rjph@Z)%Y~?7=pg7Y<)qQ~Qk>5)&YUwPS~$pZvxL$D+ZCk=30;363Rk$g zbyHjAtkuie?7}%x)K#}WdzXKcddcXRDte|c8!sM+=4~ohLjE|XdIgbUwMsnJDzBPo zwFk|-tRd4v#h?GGnu^Jf56c6>m=&nilUO?>TFI?AekdQ+HxF4`MB#y^2kCo~smpz$ z$q|;DE3iPeQ5I})D65~}y2@cQaHh@KYa4PJi?7ay6P4(Jo~ zVtW^{rK54Huc!|c5t`5ZKR4VZ}ct|te9A~RLpi9BviJIf?6eMttN!VT7`^g?%*%8hxa>#7on;P#S2+A=AM#}rb{mq!mNtco`e9^9kQD*oK-_a0G* z6^|Yc`u8c!icf?4gU1Bwfo9eH#}6J6$OoERUp?wSpmawutp9)2{d+wE{Xp^T-s8s) zdlY`nwnvX14Jd^gD9+t`@ZkP^O0Ncrd5`)%hJzwO^Y8wk&yY|=Xcj)cfA7J4O4$aA zi}xNre$@Ml(z$z@k&o^@y5E0HY2H1>%l`dG_aEPTNa^1_#m>Q3_rH4hXh3P*mnmhmmT=EDL9V?Ug|94rgt?lIsyTn-5AW73Zk4wVqBICprX42a zFEdUdM9-*csBoq|XZ|w#uKrLj`Q#pL@OJ!;1r4I|`j}|RWrcXssH9j(tU~rNmWV;i z59hI_O3ee!L<@p#oT)zB{L}Kc|8Cv7=KuU3f$6VJ6~^_$1#fdK|2_@k)G*Y5 zNIXBBeKVVhdjdx6Uw<5IB{PDz#C^%bf5~@nRos_i$Nx(LI;W{KW;)IO^`SF0_4@q3 zS>1FN)rD@{<^L|&U)3i)Vvg^m?!5C^%JgY0m3%K$d!zvPm;xD)%Gd8DsU8i;>H#D%jfp;Aekn(%?Sz<{{x%=- z?_`E%o#Lc$699foHi-;HBi!0N20iR+{%|;2h||}Fn%G_q=R@{#UXQIIGoNr)Gwnx^ z>*as)yn5P9>S6PeuN?#{#ZqQ#ZdMLFBAi|O#AImr$i`0o2l&$nA-d~Wy0o^37i|K#0Ld#mbeFqhr+59^V%PO~7;mU4Y&kgBE z&g$10nJ@uP>jZXj7%1(8+0I)rn70PayLSQp6EP8H0ki{4{5TmEc`;C14g(H0o>MS! zBS!@?v}#bjcO+-!#_oJJWkY&iH3Jqq0sg2L?BN0A#KpXt)XX<& z;AD?~nx2{5*@EAY!8>!gvO$TS{Hv+zk>&u;S(x?&zl^9&qr&B%N4^sQd`9w>GuUYm z3PwODZG4N#k1MDb+={LTzPg=y>IPzMPp#exFnm6et;*(rB>UH|e;zO1FD}mO<@;Il zo+nq7ppm zoSYnhN0MtSV(0NFe}C$ze{6=oUEzgU8uS-Pr z+kqIc8sw40D_GMPtXZBP7#N6sMZqTZiehX4Q9p#JhY+Qvbq(`9rKO9DYFrP`!z$`} z8pT9DQOmB*oNPt_(@mS+3`b!>oH9UHYg6e)VWn5`}9=`p7Jbz zuGU1xfJ`UAT*058{_p$mp8eNa$-1@oT_--4nm=v0wMaulwxR1M%wt z`}I)#ddPk~62Bg?UysGF$L!Zv;@4N~*HA*{NJjD}$1;{bIhu+5$?;TA@+U`hCVz5F zPb`FQEQD_@gzqebrxwEZ3c@=_hHCO~B;_S)^QD!N6e**B4*BHq#!31ToN?w&5*~vn z|M&j^P)h*<6ay3h000O8Yj%W_1w}XxYj%WJ;qGC`??V6p@7R+|MJop9L;wH)0G?J= A9{>OV delta 17376 zcmV(-K-|CWiUItJ0S!<~0|XQR000O80f%sr4bTn&hj3SWs!4(VLjV9&*^%pie|Nm) zo8{zrJzCs(GOw3EPOD`-zVluE^NZP}`1M9noLAH7uz1e@%bq@4u>ZWS#;f_F{<-R` zzb@)#*)1mG-vidXDCX6tRXwj3MXxw6CgM@mELQvp?#sFz6elOey0|Oa{i?eETn*28 z(^s=a=itbBX#1;IhO%a|8ZYZvfAeIuoOLGMg27)EC#Sg6N+VryqyohCjl?Jgzymap zv)O!jeqP|=7r%bJoYx;dRC76`>*DLLi%D_H7;)m#v8Tb)bX-ZSqD3zAH3dab)Lq3d z&M}f}-)!Dg=Vu*K7be9QCyF9X&xB*iUBx{WXwzymL1+zmP*Se$SMSZ3lxPnn^Su1H2h#%{OjKnx1 z8V!_Kj7BJNdWb}KF>2MF9KY_>wJ}pAqhsJ5 zA-t=2Z%-n}Auku2HU#(;0>8qt&Bi?I^Jl`IE!ilci$9(#^Fhih-xc*o20P1KZvQNC|MPT(&cfo@2dO^!e2KZM_vz*gb# zJvN-3!g(=TB`e`W zHJo|$nmdVMag$MdSd7HKWziY(KMwd`PLO}Q=;)Vx#l_kR0OG|^K01_tjl^Gui{s(> zSTI=g0^?*bUb8;{;v>_Jw?Q;%tV8z0f+-~^-B06DT>pO6Oor2{Sq{(Ta#+H%oQ}23 zYK353tAE>be=JY#VYQDd1TX`Vv~HL%V=*FnO6iS|^$z;-`A2h=KN!cjw;Go31%MHE zg(k9L#l>%f|AY_s!XQ6;V-_1WBF~MYt=s0SnULScaqadV8Z8S>G!>Zgh>wQdL+dSi zF#(ra3A=oCzFPdyw9cUQnU}Li&;)EDgc3@j42mIx)HZ^Mg7ZaT861~|NQbcYbSlpm zKp@qGtRKf_DC?IY98J+a{7{6FgbNCVh$g*(7;d?kxj@QWAg{%e#21ObG`^IJ7r64F zX9v6de_L<(6tNa79=Rgzus;sjvJk-whxuwKJ1+0|!qP17d4&FP5$UmG}vIxd$Bs# zxd|5f)=MXQ8QX?XnN7QkAs>sCzm}+_;Q$b)D6vmu&*Kx-%UR368qSyB%-90F@3>OC zf9@7|F4@G?4?|A?A7ldG1TqeclW>170fhb44+G-q*|FAPJm-do`b3Ftw>Ghfl6P-L#Chd|{5EsXh!jQ#vZIyYV4p zDxJ0=7tL()WHMR60d{5AZh;4fB$2D+f9-f;6r$0y)@2tB*=o$Uv*~oT9Qq1l_#){! zmPu-A=+?ne!*$>wUxVb8#g_m#{xV-RZOPBDls zw4-i_5Mmm2LQ~_$<@RSQ@14Iffe|}1@pdG*%NINCB}3iU)pS@lEHM7-1=IQce*{&f zjQ2!Paob(WGvlCUw7hsrLSAXegT1E#GA+o&0C!4N`#?j2P05r9f9qnhC2H{2X2)Z#cRbc=v&3I2kx?WqA+PBck|M}b z)e@jcFF}5|8uJUPBq<2Zkx+yakzA0!eLq&K+X=P04VmINWu0T8T7<0cvR5i!$^Ynx zhIYFyXYKg&a9+GFzLvqE0sss=825T>&ev@8wovM|piPt>B^V9*!AP2Me`9!FFE`wy z2w-Hha6GLmdWPqV3NEzNb4lN^-kA=s4QZ-%omWSZ#)#}GI`O(&;xU`)?2i~&$P5L5 zOGIMf>ie338VgW?MjRE@kc;`F6!Tp|%%uLqR%TJbKuUE~R;6HR+v*UVUQ7Kf>5lQH zABl9uSc5R5<(S9el^YZ6f3m(fuNMC^Z0g02o${kxm5zxLg1A;)LlP7Xhei2O3?+w} zKhNsL@&~3nPHBk*0d?F(rO~keA0K27o{#3qVlf-nay`z6o`a?%@w7qo*Je21yc7%n zS=0I0Ris7`bs(ng$CNRoj%8gKk8WQUyE8hNBFNOO*KsP1Lx|CofAF=~=maCxlpqNR%dxDdGqToIE$~(8y2LhFL*H)JEpP+~=T-grM7XXP)oGb1$DE}ZtB89H zE6c{(m4FThco48#e?&A;(=kk7N6c0TQU4VH7uw5iG-WA&v zC*n_BzToWYsMpz+M<&z-(o2B(P-lL_pfg=f$AvA;R{VKW{Ao~}26h3n_DSFdkvLCw z6K!A+wHYp5U5^b8sX3fWa%?~G+@wfmp+LDDYWNK66nHJUI5+U&_vwC+mkJufMq z7PsXHM2Im`$$&$5bYag7Ll2FOT0eQnMtTL8hbmPlpy~N$qvs0l$VOp0)=~U>S;Eol zNN1hmf21oUHCma7hC8mDg77sfI%zD)r65A$a~q*Zn|FFz#&!=JC%{I`#Un2Ym-KRp zXPS4M5OB*JT0H0{vf7)~xV#F>$hIdqF*qT+xTV1CC7 zi1cvgEkj=&q^Yz9HmSL1LqoHFE6(-J<+(o3R!IWk^tAu0gS~DCi;uJ^XZZ ze>)F}+ZzlHaV>w02F#5DCb*GHg6P|oaIgL6J@>h!qAO`b2Q)*}deL!!ZnsLps#ljI zOdT%6di?#c8E?GkxYe3$eUvCLz6a81H{|d*!SWlS^ zp5YBqeFsq{1M=esPcNLY5^JxKQN<` zMx|xi9ci4Xr9eQ3LUi>)^*DZ?EemqijDt(4W@ud-shkzh zEq06ARL<6%eVv-=+mII^jI5Fw7Ix zu9gLGTv4FBC=&qnGyje@B=ZJNm*p-B6xN^5rao!y`3%YvS(5LjJihL1f2le#&B;)l zWrpI=1%8UCpX^jkmIspukq?WX#AOg`@k^9XQ2Rh=8A2~Feo|{-4R>YWt_)mK(A1#P zQxzVqckY6X#)&(##v4aMN23YAj?_annm@&3A#eaT*IAHx#2q$i#5G6ab|jrpJvP~I zex~(CD$N+(i}9eh+M7|me`7l|8bOJ-Q1oNFYqN949%Jf6Q0-w4LITxQT2VCZ_hKRi z7u0}(W=JL)>0r{WaW(N?pT{}w@0lzgh2$_rz?>vIuMdvZs1*MmiqKtT|4 z6nMuGM}%#PcUR^7$Tn8O~(LlJy1p)9B}42 zbiruenrfa+37$FBxGWN5ouX)vCX|Lw5|@F6;Jq7F{!{b6e zJK!bBfwY@TZo9tQm5R&kq;z<6?(VC`B;>oZ&QxCjK9$viHwlj&cWgcp>0Mio@gu^+ zMQNh}(!MSLh?qGDekO&$+VWI2x#BzM0Kc+ya0lgc9NlgbCi_kGu zfS)Kgf3u@7;bW5eIA*t$%;8fur%3y^qGNdDD_fYOBI_#BHm}oH8M(?+g)HVPF2vZ z!&2N*f=Vb!F~YRsPF7d?be3C4(bBV<0L!S=f8`LHFGK(_BFHpeN0>O{n=Qv(&2jI7 z+=DrWrMX{8rlq*01ar+%-{9Qx7`3h1alTXrKXY|x&KrP6;M@TX#2&N=gLd?SK7107 zo%pDCI3Nv(amr`5Wr-*iYtM?z&w>R?a()M5$>nq62==dE|2$s2UtFBm%lEV9ef4uS zf8V^9X}D_x=4JJP{a@Q70XnpmR~Yp9O}|*hRJN}pZy41#%$Y3~m^~z-cK$ze8b#Cv z3P80F$W%>8d`77SQ_ng*$#W&-8mQv4#q)}PowSzK0QOJb;jB|@2(`HTUOo*#sk=oF zKoNg>P+(m|F#C1}1WB1G67I5|R?q8cf4x)-wwlrN;5tyoWbPKig6lz!o#uM=5m$a|r4mgl?y!RodIsqcw>l7~LMBY60=B=6c>e{P#1 z*>SKD;vGjAQFL*$A`|vJu~#@-h+>#{x;=C&1&+&z{j%W4Y?DbwP1shMbr6MtgYDDU zmSHHr?tpMam9a%=Ih=^9R_7`XdtRMw9UDtpZp#2rPf?pxTpV&18&h^Hp{^j*RXAaY zhO$FcZHOl~B%`C;CLa+6>lc_Ke{rRwX47G(#gDlu%ZB$mi5TvBIdE4RZbHbruARbC z&KT-;a*hHHN;-RiWP1Ep)l`hW&tlCj#^b`vR-niY;!y+0U>x0qQvsSKIs02V7ms6^ zjNF?WYEM8=jg3;aP~=@TI8)=IG={1Bj9TznCA^LF@)9&pnM8gbo>$Gdf7(rSCnrh| zk8Lu`5FD+uh*Pzb$fT2Sqz3C#0LkWMkoN5*n2*Vi3z39qk$(7bwpbPy^J-G_tCI>* zg=zX_h7eS#%oc(TlS_1^caS5LU*?U#Jn}f9C_>}(8WrkbwfJZ1pQ&=@v&-OQC0cAi zi`0PIUfM}$eQGqIjEJdVe~3ZCw`DUXkH)JsTE}`a2q1UnJ;;|yM<@=T!_UipjOF_J zerAVT^+$J|E3%v)J*%4N@eugO?GVR8_|s?YB*UX1{0n~Xiedwge@Kd-0(8$n#l7Ec^qg@XMj8Yj9`5` zBPMwyRW zE5T#T>E!>gn-V#vvg^_q3}$1W4aCNTt_Hcy?}1Y*G;q3Ce|sa}fC9H~dY~P;>YWbQ}1-6T0WLX~Nk<^$>Y1K{45*9-J%^bBVZ`*L{3SHr`C-QjBz;8Wch z-{LkR)_Izce`H&tmq?v!Pt^;~Dg8eCi`^N7hHexXWPFx_pGvf!^ZuQzs>OHEvkeV? zQIxacfYSZD+Rjjn6aA3AeG*@SfO{RV6zt?J@LY;wlpyp3a96}3;G1xmL7hSm0AYVc zZ#hZFD;A)r!qFf<%&W9S22N})^5D?(Q8r%!+;Bf8 zzE#`U~;49!g_i!W9q?lxv3_FxD|0( z&70x*e*(Pak6%77PSAU1*XMOp4d*@>e$JQx^Fn+woq>VxV_>)q`C#l@|DoEbwB6Vs zr?biGyehsMo;8~{%gOV4w7BzRUN3)~R?B*P2aZYb?~G|PFUVl(GrJgmT2;Zusn$eftdl8P!#5gL#k^=;5V{Ap0;pmEk^nw#E2hjH2sEx*~ksm{+#TTI}U%M`Cbk8#iUR%8&xp>YxoTs1*k^Fg-I6N5~w|y!8B1esKP#&<*bOo1>y5a9#?W za+6#4hKjV2qq@2(I*o0AnC@dL&BL=Ae{tR>PJ0=qz4YiPA?>9hzL)Bt@0n|L_CRUT zlhrz+NF1}(A!MOO3!Obi;H2;ZjBxMangEpN?8c&(RQxbUGPS^S3>&biK6@$fJ zlHHca|0&$k(SRvS{$8+e&}r<6Aox)oyRs#d=JA;#$4ULBlg8E_s*HK4lJGPo@=zYB z@lNOf*ORXsE;jdZy)RHS%Fk$jb0&Rfd0LESv-2Qz=8+{&C`RjprZv>5gS{M9Z4!r7 zd7Q-;dEmgRencEvlM@^&0-wZ_KO7Z*WU9SHuh$}wgeKlbQqZ{x?^UamvrD{?ynnpl zxqDc|D#==G2NA|=c=+e){Gyr%tX5AlY3qd=2jUQ|Xo1F2O+%3%*0L7hN(;_Lo)NQD z(}I_nXS6gjGq1AprIVHy4N#`i<1wR%Z#PIT_tsnRLVtu?}x78otKD(uuF9NC1e%yr~fy|HGGCaBbTHx?ZOX=y|L8Hnf+B z_KcN(OVUeAdPbJO)k7sUD;T_g)6PpC0tzXXe@G{R3R^Ak7Tf~W#$Qv5q|i@1?ekM% zRmHDGp#mA$PP_1*I)0Ikz)_pKh7>7BH_{ktZ;Gf@gdbl0PA2f%Y!fp`ppg8@n&!9A^RRI;yYwPaclx8+ zxK7w>LxiGKn=qW#w~hYyYPPKTRS?bObu}H<&7`uQm&W%FGHcC$OqQ8j1snX_+%L$5 z7r2fR8_*nU1j?#>vR|M0q*7L&Znzs#PT7&^riBbMmL{=zCvcWwGU2@b#8s+GT^$;( zV^@=w8N1lx`y@|P$VcKaf=G)-&Y6maIq;w+E%XUZN{p_+aF`a!;T-O3IEQ*TW&Usu z3rmAP9At}b6{ewoV{Xa}9V>8i$!3Q#T_xFQr%;+-y^Mm$o3bOU{xc7aE(eMsNjI#3 zgnd@~%F3HNRaPpzm#Jz>-A?VFx2&Ly)0irT!88U6U<`pOS46F8TI`CWlE|nN$~#C+ zxu0|+=gy5*DzT4R$$)lv^^r(B(6q}Du0OFUZ7#9ix`$u68Y3X+Dd&{`+c7$&rZMcAk(+CFD}8Ou387Kxi_`&?Fs(R3^4{v6qq_ zaAe^>qIM#GP+sqs^tdHg|Jn5s$&wydF?ZbR{6j6bDCzk_Wp^*>p^ki#E7{hENp~p+ z$|$*5ImJFy$;Ij%o-y47i!DS+ie0dYf(Wrni=71BFrjG-a(3JJCqY>Qzv{yw1RymKxK`*v|@1t|a41H3HcjV_nlA}AdMrH7z2 z2(UnbT1F%aE{zCDHZ~&n6Ldk^oHI{-_?fFi9y>TFYIq5W=rVA=jOC$1UBUr}KxjU4 zg=7bxilnQcO)EEebfBngfvzOcl?1vnfUeAcL|2ldE2+_yKDu%%bl&JnYILQ~%#vUx zF+)ebB-S|_cqK`FQ1Yao4LaT-9WQ~svfq}F>YB{@+G$Fm!*fj{eVpM`6xf(0#?!wU ze#PR5nK0o)iMw)q9)@NZ(h-yEO7HtMIV;M4?hoSyc^1t_v|wUt&6P9Mc5qT(0VFJc zH#4u`$X~7U{>`P|ZrT5DsTtcY-|5x!aI_F#eJ>Kr=;!rvd0stjCiSp+Ib7nE^fyo5 zJnbBa57Z-Z$>+ss(GT2u^p_cfr9ODH__|nBpN=Q>hkAKxfSEP#)p~K2UTbTnft&Bt z-W0_3-F$ZOeLY`rtYR)!gdP^=skcCXcZims#@HXtuV%kE7fL3_B1qsvc|O!5IV|*V zHYf(NBL~)%lx%Z7i^25tQ&?C?=%|^v)dw=nny9+73N%-W4_}C0wvb}I;PBqQQy`p8 z2G#(w12yIULsvWU{~^MTz>5?YVOt2$5YKy|R@Ve{_}(a97_@RMVLi6h2tH1KEEU^I zxAFFC@|m^0GKR+*(LIDDW4OBzMe-T}q`k-I96Loslnq8SzYY0HO#=wIl9~rte~+>Z z$@+ME4QSZZ2;Ia;w`9P;_DcwoO2+)ari1z4h8y?d(X{Y_^VN>(lxa(}>%i+r5TlY< zBUg!{S%n8mpKUIoF_P(?G!0IFqAoOLMlx@2s!z|WrcchRCVJP=1g@&}$%8RWf<4(& z3Qh1JkKjQr!Myrm@wWfYXn1-Ah<)DFK#=|9f4SQf zG6UHP&9xNfBlu2fUgQ;LWRGxMrm<6&k+_SSocUX*HfyLp{G1;)9{a?9yUYet1B$iv z;DS2i#5z2YdR{fRcq&!TZ!pPvG5dwTg7om_h7(St6mpl)E9dwLD1l(~1%ZZiFa#(P z7_lMizQ=6`5RA_}bqKVyv~tb|={gA$<}aq)7U;-~+r}k8iCrg!0TBf5#C7x#x~owj zi4d4o)9W?H-&gbMtX?~R#?~!ru{@{JBqjlmivLZjg& zm=9owLv4oQ#o`xm4A3?IO-`hCwPF8yHD|^FAIqPcMPlj(4>o%XlETw;IDDd`Bl$4! zfs^C}rDf#B1K~v@2p3L5-;K=sib}u=7hITa)nD>R zRtRu^EG<-=(q#W~&)k!XH93%9eyqLXA(R~5CVi06}#l?$~1<_=5-Sv+osOe^NBO)Zo75E<>R1A|kx z_Juz{sLFYNHl3r(gcd*Dn-T{SbJ$&*YR84-u~A|XH1J(ltvuQ$0yz?6fSg`>QjFM+ zZhtmpt|p!bT>Jt*2|unfa%`t=QqcXZJSMMOfDlv$57xLrD#b3EoFt`FcZA4A_g!Gm zs+6)laqwP^sDCBI%Kyi+x^M*q-;smxXll24YzT*cNMTAn#ezMcqsM4I+%EEc@%@MP za`G24&Vq&5P5*vAn=-f^IfWeXIyq0@jb=99Zu(m}H@MsB=IbA5Go3v(pI+B5-tu$O zlKyv`shXVPE-($(PE{+B0&hT+YCm`+=;V5MWgs5N{G`+HG|=w(?1KsH8!m2pbCfaw z-2tqBj|9sWe7dvHjvVIw8Zpf)2_QfKHbaun=B=gX79z*8)r$-va`pSxm7TTCD2}xW zc<_m#+xzGw@@1 zWaTY43{O3&o_kB0BIs5?lh8)CCmchZ;C?VO#NMUTK@6r$WRUI&cyh~eVG-_~C!TzR zncJNNPZJc$sAWhVz)bsi0KvA!8A7U8P69Ko9j>$}|9DN)2E0fH8U88pCNggq?)M*m zVpBMe>etK4+u+mdLO!XdWBlV2*V}C5T+oDccjHCDK5fE(GLUe0 zj9J70hbuQ>yWlpD7=Lv1wJo3g8$bk)^j$G+`Sh!a8=C4D=7LOS_0X`*UN#`Pu^KVW zc{!V1NI1H+T=aLnGpN3e>KRZX)Rg0Y6(!g&hVYmNB|k3x{gpEZabd+PorviudttajrG)<1&YmtF{k7(x|6CA^*Jm(rJ%HniYnOoe)XScO2& z2q~#uBdp>2KpR2NQ#Y$G>Zx#$balrYFEfc*;FWSPlOepeZtl?Lt~(_Jky%SbpUJ8r z-_w}s0Thxr!Acf+U%)&+y(P%gNjb21wmB8yl9Ma(>K) z(0u5vO}sQ9y!WSb$sGT9wpt#4aMd;#Wu~sUx>Q{`2z~23Z_WShJMjY0sZarb=j}Uw zbi)l76d|`5C3OP{fxC!ZxV6H(jp(&lP35T_*2nB19-6&Y_LD)BO*^dZdqz4KE+dmY zw5wuqJ0Wi;&X)+6%Ku^$x;83eBZ=P;}4wpfl;!ngFpf)*^ zF@L3Q%u-Cn&BB|Nxf_Y$mE)!7&jg0xW3gj@nJnl^@|&x-l26b}lLdFg8!kS^TLw$g zl|>;7bDrv5N@4dN`@0-}0+os4@{)*zMY;XFa<}$HZf;#FDj(oOh4}KS>z*tYvvDmV z!p>MY!_X+{+)HcXf_1dsyy>}{G>oh%lwX|s+fJbpjQJA$+turs~MF~sG5=;X4JH>_cWsd8RyS`sHLmo;rY{_Y>63_ z6Y;yxs3|QYCdia>1=U58omMMnYQ>Hc_2WQ6Z$1J4Yfrdwacnu^mca@4aEA#uTP%#~ z;55t;-!AfD2^q^ym;0NXOK1K&{AZe+gT&=e&MiDwU~=}ZqP*lXVc1+n9 z#Yyq)?EJhE^Zw$04u9k~d_May6vy%TtL5gRlH04SZ*33WgHLOz161h?@(ke6?Rb16 zc*JIQl_zCl)OjzB*32oqnK65jh8BZj?8Faf_uQB)-{+L^fA>G+IXK z+YMv%$CwQAkiOh@8FTo|D8USH;|576zd%}ZhzGNPFFY6Pu!FbQh6@q;g6Ngv2L#ie z66av5(H`iFy%R=3DLh;JFrQTOYC>tC_;stLy@)yNR!rfJPwk`I)sS95KLKJLb@0Er}MyfFbNp2eJ*G3w|Yfo5EG32ncmb6s@K2rkmlXWCW z;^rzmZ+k)#({PV&7^lH^3tf;v)qgol0~A5{N8Mez=FaNZ8ot8h=9oAu{(9TbH9hLmll?dYyC= z>-nh5(a_)`mrmeI4B^$fk+E)b&n^j$y5!YwNP20XyMzG!tE*|s;O)_9HdXJOvj@)A zgWY1q?;u@C@t=sF81{<84#`S=tbb-rC?3DYVD0aNbJBbMe#e8YwK|MH+hoJnV`tFU+K{6#eQWjx95mx^HoV^A+2S7=WB1iCu76%oL5Xo^ zfD3ZON8mF-+jq*3!Q2sjU#qW$9d+BQxjY+Q`|N0+gQ3emJ98PHKtSVMWhCyE1w^`h z-I&W}lOx&Up6UopYSsy{CL%8wEoMaz@Ur?8#68%58lzYw)y;?0+-dCFJlhb@)EDz^ zJJ-`oVov!h<}A!#n~<7XqJJV@Qa9R(O+8VkBzN@q;WtE|oXC^JhdgK;HtAbQEWWP# z{0Zu)Nz=#N3I159FS|>vNS9$ndWsHVZtW;8yT~aByjlt#8ELNo1{4{R&tc29EJpwi zTj#O)SW{)5UDDy{rD%%AOoyPCehA9@uXO)a(9JvNXZIz#W2N$!n13K*KxrXjSfn_Q zW8#DY$`Po0vN&6;gj8vv#^-4te|)N@PeSial7{(Mj_t(=0MSB>$S}&2pd|l#aZ$}x ziK`;$f5o2;m4CMnDPxs=+zF7q_&f1J&Vs}ipgQnWf75lVE9emMsCgs5|_;${iWCahpiPu!0%= za+N%Xo7)o~f!@_&v29Iry(`I<|ExppRU69&*w6*WUAf^9Y=3Bp zR_z$jY@~AQfJT$l335_?7bL*KL>3%`JQ~5(l^p(o(N0Gxcc8>qR9DM#;v~J``F7U) zT+J6%XR5{$&3_9_i5$RGr^2R09^mAJ_{bdAoT<_rE~bs<*9t6XPQiMn1&~t&BxbEgGS%IY!f1X~8r+>x0%}Ndq*g5F z79K5R#qjTLPo-l|aVodBrx4tfj0BV0%Vr-wu*Dd%6%sToy@n;x(4i3^h*1c@d(E7$ zdwcsoyZeye%*lUtt^e$5_Mry=~CBpf}RsctH82y}N_r@D*Jnhvt znF5{YN{Y$3+G$HU^?f<{w1?!>kI8A1B`3i2jHP>)fU8236id!7XKxF^oG8ikl9KW6#@b#s{>CFgdPF+0EyG@1K8WW@ z3H`Mh&NnYb`&kp6VoDPPl^yZZ%=~4pG|H6)u`(c50z`0E84|dKSW0grN|G!jl{Kao zMXd>V#Evdze^OlE4x4dxzIdqwOglR-YJV*QQX+U8kb;YMKjnljUE7=kC?nkUxs_xv z{EXAC!}AvliIQ@vI9U%E5`OQkV{#fz+{wto}z83p49Yy#&Q}!N$G+Pa1 zx5dn#x^ie2e2IAdbHtgSZTT0kMhunrq}Szi3-53OZh*_f@jK#9)L=k)L=4Satbe&< z^IpPpj&e<3h?8N@nq@U_hHS!{HRp9x4T&2vV6%*)j^apU=qd|wU{i^^(zjT!zXbjE zPv_6%@ATR;d3YKW2Hy**s(_$c^;*wzA?`yZK_f`6yey3 z_b6ciIHgpP2|i82ias3w%76U?U|=Eu1NS|+GJ=tDL-f#NGeZ*o72t4~$NmgqrN^5@ zr@|+b$-)Y`uWq2J1_5K?0Quz`mDDEl=l}$31NS@em0Z05pJgtV5y6gsq#eH38o;$|i3dhIMiGLtTNJHwB?&^>g z842cWJGMB=>4+z+`xy?vF$%&|6;c=>=2=Ouk7z+cEUL^kUDuyjfdXL$n94W2Cli@+ zO*j@Cnf7^7uo?v1O(|%GRN?`I-3_Uc)xeA*LI0kVqtueolU0~srs>iqi z>TvDCRdnBmlxAS!A7k6R(BHOlpmjn26y`jMrdGs8)Hvvg2#)R^vlK-zh^zkeC!;S2 zT}x#MM3Vva*n#jXpYDJs&K`m9je!;BnXS?yzL_;tosGAb$oLo*)TxC`JxcD5q1~usEihDTk4s7RIhq6kN2sX}%*-0BBd_cvqto zCbmwxpi~Aeup6@_Rl#sO!&SPD-B*{mUpID)9lMvWfn*IC`jO75DUvD}op{l721^4; z$;jv45Ghu1#UpKL>UBi>Nk(+3Ue_K9EuhL>-X;w@wSSIIR{2sSxzu#L?JwUcVYy{l zHsDm)v}s*(Z9q%USZ0=LB~~(RQ3uU0Q_o!!Bs3|JKg+*V@RiKN_E72XLmB0*Fh%)Sq^9i7oyf%V?%5Bd;h7DzEQTm};Hpd1N3(V8fk zaa;esOn()aC6JlYByqXhCE~fR^f9Oq4QalG@D{h_ks>=t{RAK|m^WQ`zd?90)}yus z`qV?ujp5fev4@}gxg9)@Wfop!m2OarZLgj^GmXL(bc7%A81ZQD}IR_EtGtd^|54Z+sxU!3a5DK(_>KRxNU7)g$jW5_d2{H1dlqc)i%N)HVQ`QK090l;0`SxD(nS2xzG{Q zvZNk1v|y&|5+BdH)aRrEl6EYG)-K0hJl z6%vWMpX&t+TJZ(7VlX?bzy`uEIe#C&T*GBMUAa2&t5nvY=3;4^)-4Y`vYj-u^vC$ORSAmAr2!*)7%9b|AG3FTkb;t=f3-KhG0)l7!ds#y-t<;VHB zuO)D2?Xa~YkRs<*xNwj}kb=hsWY3jT#AX{&Mz}JFRBI7-fDRXgjT3F8(0@8&>K#!P zmoi!TAsT3?YTqT(3b(4{+UKCIa>nF1-i*;vJCVNUlpB&c6<^GB%xHsNRSY6naCyLt zWt2KnMV3;Eo?5fLeQfxW@JivGb+^7zZV|Y=)hU&3 zW#wrCu7GK^HZH>OjmlWD1wO(Y`rfkA1A8BV*Wv~B`Q~k|Fpy~_`VNCZ$6Q{({_DCP z_O@+Jd1qiqN zRmh0u4*oKGc)vq<5vt5kypZLC-e&foBTu2-_g~x-FCP0Z?te=h5B)a}#G88rmWSfa zLjuhs32i_idMs&vKw$bxyn4_lQ1ulLdIJJmU-6-LpTO5wyy$&JVC*Y?^uMBTYM$JC zOd-{LdGwINs(AC@!95DC;?KQ)?-7Mq@#x{8f1kpv_%ygbcub%kXja{S{NNFRe4x4Y z)ua9cN_P~)`hQ>Dzt8oox7(Q`RLxG`~An1=G{}g?B9QM z|M9(tl>XgQ>>PY`|Eq_O29y>)R2+MJ|Ng^A_wRFjy??JBJm^0Z+zWa!@{)@!qO-_b z5qE{+Grpyyw8Mn_WyUFl=ovK)71y-q%wJ~T)gS65pXH+s-j3g~ z=t0zC9}_LPtPoEcl_m>`RmeWZ5;17`O+D6B>3g7=XhE=zGu3CCpRC|)Vo~;&<(K$5 ziLRAk4GjU&K3$B57uA2SX8gbcCRP40u)k%pV1HOe2lo7q>?uM2dh7qbyu~p5->qBM z{Gb0LF#WZu!nl68;BAiO-={&G8ipDWiRXv2Z)P)bbHIrG>yLviX-4qgxG(uSK=K`2 z9`~iF0r--D&S~n5nNG8RedtV0y*~eMRyUnRb)g$~`M(SHSM^Dcm?V>{=;F$|=u_rZ#_0nXox!!sihQ!EEPGcu~r5;VzV7Gm)N=$yne@!oNb}Vt;zA z(6Sb9-$BJ@Hvdk;vdV3iy0RPBb3^)(vkZ1dCQN|SI)Pmr21+|&w)0jD=B)v}148^k z^X^@M|3plL8BRt;UJTTh!+?X0=M+o;$x(rvtr}GC9m!d_)jOX}*^r)B&49&DfIsR5 zdw2jjaWStZHS-Ns;lxIo4c%f|H!Ec`IO~6-re`L1w(>V*@XlPWY*3;n|DdXRq&dKo z7p6VIFC%KxsBrn`k?%wRpOJj!40alXf)UV38{cB`;|l5px1#HTuWqNFx`9~RQ>(WE z44;o=tFk#D$^P~0pT~>$i;MGm`F_^CX9_&uyq6Yz4MXKOWT>1OEW5k|n(P?QV2-F?og4}*y7te)K(yyx8TN>#e76P-9kdG;D~`b2j20{ zTj59(Lpnk&{rVvPfcrK0-EmlL@|b^sLQPFlG|*?F?k}tr?h%$jSXE6$co# zZg~xDj#^?;(*XCQV7=+DIF-+H-+HS|+QVv($+VfnL++^TShbU}id?;uu2;oF)~4iK zB>s?dl31}QP{4N~4;>Eai(nbS*m*q4-=8||S@g`_s&IeWHj;E- z=`fl(FdZKKQZHGYz9??%l}0$c*XvrvQ)f}`h;_AC%IBPnr6i+URO*ou_Zz(&%b79Q zV;~IGP|g1qofGRygx$i5#ZoJz14-5N(ev#VAYA>22?5J1hbbz#@Wvz;a+vdGHm$6N zc`RZ*DuO*~{VVhVzma=!%kzKY>k?7@b|40<26-g$3fA-mYnJB+1_okZQLst9q8J-M z)DI!*Aw;QZUBi4&Y3bsk8rQ?~u!_2#Mlq33)UvBHCz}z#bdzdo24jA3v0%YPXKZh7 zcKi_GdQ4M-4T{4qb#9%=K7Eyfr##D_t2L1^AkzsjSMcYj|NH*CXa9fo>@RPmhvP2o zl;;S(?DYrt?mu|==puJSK>T{ZemxYw92A2;1n`+nn@GNr@yhR&f}wp+f{v|o*BpOt%>Lu$pe#nX5m zvA>9E+wffMZ}o9MzM9fkNo9KNhL0DieDTYzaag!&=IN(GQ$N)?ywW;;O*Zaj{dW0z z_n#jTeOxYNs`B6H;ODnrY_wG}C$K)t@JVoOToUD_zT{$I`WLCizbfyAC`AB%)VvS1qr_CwMvePE>0?PE>^+QHH1HWR=jn`wz9$Mk?%U6 ziP{hBJG9p@q(7SSH{^F~++oQL>mtu>wtNtbdf$0}WBB)bMq&){a=Twt&pg=hafw1nUvA6+7bTzWqfARn>Ks;S zwI2)9k8#;8-*@}z5!T1sg|4cE&wQ{Wt!m!0CXo&q<11<#Y}_aDE)@-Wz2jC!14QkMcVzj7PY=j+>y7zk^9gs$LJf2k5uI{AKRfaZQ7&q_(xHqQ#@x1Ot|y3 ze*f=yA(jb~V(Z%6{~w(HLs*;RfKKUw9RfA_9Gi8zKW;fAp!aav=B8KsWlySvRWbY5 zbGh<;i(2|I#(mLw4RdRi*;fTKXRq0k@;LKfUcPvwp&o_vx)g zdKSh~+sZFrU-fT+R*Viq+p7bY*%mdqZB~CN;v(xb!RtcJ`&XNv39s;4{4~H)xT#w} z=$tXXQ1K;?7tB9wef#{^%Plw=aiUiHllsBw3%KgDTX^3y#&~b}l?(V<7t9R;|-k!*@!>N=f>!d?z}GX>#lre*QWZ;J@eMbE$>kK!5HAp$RxrHkF3dEOcuN- Qu{HTTlMY)66EMOU0A2CT<^TWy delta 483 zcmeyx+Q`Nm;LXe;!oa}5!NA&HFp>8{J&+2YGJB$OGa~~-77GIdJ5aKqC_lX@F?Z>d z!0cuNk=FZvMaAcfxNzS-TyQrbS(hW1JvXsm=yk5N!7OO4&gLTvz_0vah>-0_c zxb%Iplcne!N#5JLrAnXvb*!|AX5hIxZ#i!mYj1`BZOx8b?Fv&D{5*Fx`>blfRJYR$ zi%c-O-op^!!L-ib)d2zN5mkp=y4y%9S-=yy-dW|Fd9`lZfEuXe`{CXB@ zysUAB70k2W!Hp1+APO& z%l%)k=c{P6G?*pe5x8K&+*1lmRzALXC7b83x5WjK)c*pNdt>(Yb*lYf4De=T5@CkN X+2m#>3tp5+n|y*vhpn0k7;g*!3U1FI diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo index f4f36b7058b07606d1bd96c3e861c4713909cc3a..84e1caa4bfda39a0c8a3a13f7e77889c2abcbf4b 100644 GIT binary patch delta 450 zcmaFP`hb-;z?+#xgn@y9gCV!9Wg_o|dLR`Z#DCr{iIIW9k%fVQ9Vl5)l%HOdn7efH z-K=H@f!6o6T?e&UFFI5Q=0s&EHag69l6sLE@mM7?BG!6$Tg!y<_1V7H)x2A2;1n`+nn@GNr@yhR&f}wp+f{v|o*BpOt%>Lu$pe#nX5m zvA>9E+wffMZ}o9MzM9fkNo9KNhL0DieDTYzaag!&=IN(GQ$N)?ywW;;O*Zaj{dW0z z_n#jTeOxYNs`B6H;ODnrY_wG}C$K)t@JVoOToUD_zT{$I`WLCizbfyAC`AB%)VvS1qr_CwMvePE>0?PE>^+QHH1HWR=jn`wz9$Mk?%U6 ziP{hBJG9p@q(7SSH{^F~++oQL>mtu>wtNtbdf$0}WBB)bMq&){a=Twt&pg=hafw1nUvA6+7bTzWqfARn>Ks;S zwI2)9k8#;8-*@}z5!T1sg|4cE&wQ{Wt!m!0CXo&q<11<#Y}_aDE)@-Wz2j2A2;1n`+nn@GNr@yhR&f}wp+f{v|o*BpOt%>Lu$pe#nX5m zvA>9E+wffMZ}o9MzM9fkNo9KNhL0DieDTYzaag!&=IN(GQ$N)?ywW;;O*Zaj{dW0z z_n#jTeOxYNs`B6H;ODnrY_wG}C$K)t@JVoOToUD_zT{$I`WLCizbJU?T5@dLR{UbU@B9laYZTm4$(U9Vl5)l%HOdn7ee! z?W|@8fwuRxT?e&UFFI5QzF~}-<)GlJ$oa)+P2nV+71`<6CkT9cSGxA)ts`MhEP~(W zA2$E5!^U_dXXe`n*YfyAC`AB%)VvS1qr_CwMvePE>0?PE>^+QHH1HWR=jn`wz9$Mk?%U6 ziP{hBJG9p@q(7SSH{^F~++oQL>mtu>wtNtbdf$0}WBB)bMq&){a=Twt&pg=hafw1nUvA6+7bTzWqfARn>Ks;S zwI2)9k8#;8-*@}z5!T1sg|4cE&wQ{Wt!m!0CXo&q<11<#Y}_aDE)@-Wz2jbcpNa=9`W9N*A6 zdB=ubWo5jaivRca`R;0JYT@c`zd7^!UURAA6S{H>TYkULlX6wo?`!NoTM#DG?dHTZ}wE%Dj%qaGOlsB>ep2_o&0ASvS5lJz%=pb#&sv zADmU&g?QH}ReYIKJmL0gF8%!tD<`Z{`m)}Lae>j+=UJN_lmFOHNISK2Ylrmb_va70 z@wZLdaj;JRV(XK5#UG8u`k#X)v&JSh$~0+st6X07#i>Y^KPKPcReYX)u*uzijWcZI03!p#or$lM>b-?ImT0Op${m(c zPjig5-rd$R;eXt5wOGfMEnJTh%kKStc2=rQpgXs&<@W%FnBHu=}`9 zSo_k$-=3Eea`y!3-tOKY`u1@~^t}IE%VxUxGhCY_k|!u5599+%u72*-|ab@v9VnB7zrb^UdBdPx?Su2|&4FaAZ} z|GeAjE#rL3?5LpJ;`R&y-aQs<)vsmsR6BJy-ub*IW=U#Wf!8&q>382{v)aE zmevf$IjS+g>=tdSC^bD>dBtSuamM8?(~{d(ovHtFA@uk5wa=`s=2W{Cv}H*=IiXP5 zc+St&)|YdhZMfx!v#v+|JQ$OYZJu;t{|T0cG=qe=b=Ox+sb^ieIiz>motO37I0p5&E+#<~I=$M?vWWk3TACosQX|shf0po-L0FuMNoB#j- delta 452 zcmcb^`jC}3z?+#xgn@y9gMqcZU?T5@dLR|IWPar+B0MSxog}hCvST$o;Bgb zng;Ee_uLnle5`psGp1Vb)uF7NF}e+k_7(M}ZlP%R-p&&_Uu?Z<^>TTjeq zi9cc*#-V+YX~&cmPk(pZI(m9`wQQQ{-Ip5|>3PEO& diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo index 2baa12099431cb12950364ca3d24479d1032a9ca..2ca3cce8e7a078f3a00e57e76ea810886c4b7626 100644 GIT binary patch delta 18946 zcmV)1K+V6Do&o!v0S!<~0|XQR000O8V|Ij*4bXpMc7#_KQUk_)O#lD@+5rFu0001R za&KpHVQuYwX?GhpvgmjJiuOI{j>wo+$R@Qf_t>$M(RtaPr6e<>qmxTgEvp?a3Y%0& zTe`pfp|BQ!0=k=$vdp`4CYICy3bmt9*gpR}x$Iv}R!MKOyV>4sKl}Xi1pb>}XFuP} zrtg1e{qeJB&&Jcs#VAWo=a-wWX8HVjoXzv$=9~QXWHQfYlm4jqb~+j5ldL~WK0Qm4 zQ8pg;lds`lR_VK|cH?qC$tUwBD@&4D_Uj^_WkqtCJU>d>{986D7VxQ^FocpL@fkqf zKl9+dUY%y6tI8lR706Bi`Fv>qB>6%^S;ohIxO~N><_*hnOXUxw1d4pqovb zK z<7_hLY+$_r9~flD=!zm;0{F}1v!ub9-ArDvPyd-*20CoBK3+{$^Xq)_o))qo4T+f( z!Nok*f-NPCE0UyV(r5IH`A<)(ienKbE>&O4Kwqqzcm2uxO!JPE4oBXR4%b?MF8VCf zl*OomrYuIMjB~^JX!ZTH$mjX3!E1ko@Ipv19GKO>FDuDh`1Bdqcaq-4h;{!F^e_gQ zgWw9o=;X%8e`j5-lo|z~pA@f(Vmi$G1oo}uW1z3biv9Dk$tA_RW`D){c#{{5QG*3^ z^6K)kPCqZKeqQjOk-om0U1l>-c#2&}8MSdCALDe~UkAyV!UlD&H3OzZQ zFu?s$K3_#SVA+i02|s$O%^AWK3Nyym?AQGw+wSqA=}rIFMV8#mvdetfpJ&NQAxgiv z?#~*-{ba~~HYJ=S83OM&UTh?Hck=ho`R^O;4dBfX{@K_QpI)I){}P}2=+nmyn>VK0 zlVay}KF6ISif#OC9btfzPP%^!BLKA2SkJOsHXztdn+K|Uf(1WJZu*y(*`=rt(qbx9 z>?Z~P&9LLHxMNPF$K4^5J^v=1=`Y|m`GnU4SxLvVT%q`E%E4$^GO^m2MRdMYuwg_Q-?il;mTz}0(P%@*RZ^>pYx7v>Lne}* zk_Z<*r^{|{djqHaOC*1I0syXPWN%eOTJULqHp<8OJW1Q__C5Rac3Ave+%VVs^K|kv zW7TZ+bH6CE+58@hMl!CxBf_mMQ8)SEHPjOHonDzbRnS4)BO&xpl6QjOQd|XqdtWmi z2**{Qhl11Elx&P24sC4f=0m`(*Va|wh{hs_3K;F;8l*RD9$0@G+jY(ernD&3prl;AjFdG@%rag#AX4#yDz1gpagWKI>n+tcW><)VFYKm?d8H0AR zf0Q&D%jEbt>1;QXza{C`79W`zj001zgX-;utEIf!k}5wRv|9`g`!Br+QN`#vn*wP- zl_o?{#>uqD^}D4*RAYJGz7YMUz2xwa6LkllJJ#o2__}{QPxVJmPyH)~*+_*0;uOGLB6m8{`Gp?P3%GYw4-g}|+FadU78;T+LJuDT&*F^f^aoS7ADIt8fF-@PY5K?a^9#WQjEn{z&Mylr^rP)IwC8R7+A-Gi4 zz2T-7T>-J;I<`zPq$ctQ;0`ba2Ly?-a3Bj^kL`czw&;owLv^LbjV<;)D&3w=9oS0e z&>gnfu!ThDNCLNa*>Eu{^4n~*@{MQ^)fbiK<0Y5baF(%9jTdPKv8Y~hxQ&w;=NE$C zCTn4_`FwM;cL9qx1d8Xq&CLt0=*eJ}jI;Um^b(D247bH-{&hBaKfeYhL+_t6JU>gi z2Tp$_D4t}$LF{ynn_WPH4pttJz;X%8eE9%ha5F;g7;y>gx9fbwCObMu%~&*H;PU=t z&c0e4#YJsBGZNf&8#3~s;Rp6hk8b<{{=xWq)kNX>2gYB3Me#nDyf;BLXAIA09>_18 zF(25MuKL0?9wZATwxIK5bCWfHkuZ6y>I#343#iW9v0>URWKBA#LWio5q6(?5Am@aF z7_MpDrZFmX)t+PwRAsf;Urs&UH3J0wcX@T*zp6RxkA|9euGV8_1e9O(teNG(P(%eG zC{jESgs4@O`)B6gfl>T($pg>(B2cfVi^*kC>VqxK*P|bSSd)7bWY$$${HHLFs?dMM zvaWJmuD1`^c9aQ~#vzgijUY$aj9-r>6e$PE-QZ3va{@VdkQy+_buYwVCbUHp8R^dR z=%R&_b0NlG(S@M^y)s+=tXfqGJ18r(W^&}Ubd*U!|wiW zqZg{sMHRa4STs;0fgFS|u5{I|FnQ#6T@?mUN24sHH~T6W{=+{19~e{+sfSq zW1edC5|-flasmxehv;D7`}co9o+z9Id5kFC?}O4t5slmC7mn>KnO7Bu7mek~@w}7} zLKI;a@<>WqGX^i|J2ZhKyB5~|fZpmknn-s+`>#eXVGC}ifIvgkAv!1m=I2i9zMM_R zupC?PoMt}EbhZH2fN>s@v`M_V(CjKCb`zrDXrPh^+S(ZS2K&3k0#tu{Z!4R&2qQVR z*4K;k{35&v03=CT#8PwNkYMJcf<_Cybto!SArq zW_BUZ@dz$Kz(Dd&)Ra^CJ6T&%77r(6<*@pQfkV?pC*CNDka@RYEGTIp41=5nP;)JX zEb1hvmfT^d-1KJZXM;nQmtYH%?dwx=M01>W-=b(RMFGYSIj!m$_lq?L+ z(J*YpOCKrIcyV==F98DXfyf5BS}Qe4@B3oTei(4}L%WGprh4sM*p=j;Vhlkzuo@*{HKEx>KJYPM#$Mh!s(RYe ze(8a)iqu`)N@9e{7>7}g1$)tKQy9@mGXjCK@z3-$AhU{iGDnAWj_$ijjhX>dgO0;I z6KQynlAH1f0jeG*!H{<4sl{nYRAd=hDbnjI`+cl~^4NdZ?Y9&R!H0)?2o*pQz>O9i zREyCnq8!FKl(wM2xP%ZGhMVcWD^FCT?jl25<4Nn3*;E8Y82;U{gDN5p~-^~B27oh+|x87^E;^+we@fv~TSc+wm#kSUxnwni`EQl@OnY);MKHvxs z7{Z7Q>ZD0_UQ*nN7pIy>IQx_dHrt;%{wL06rcIiwfvv72TPv`!8gl}AlksX9uLh{f z%2*l5R8Ot_qxFtDJj!-)TT_u0)nqPe=_-GCPK$r)9MsicHJJod9;R-@^wUAlnt(p3 z;Si_V9Pe8d*_Z~#PA|sJFGiIrrl|LrILo<{bAO8Q0gte*zBa;&ujhFYjV9-LG_bmg zt!=~_t2_;NMk!C-qva_tSDTl3j~l#8%FRWF(*lpR8(!%~c%~cSZM8Vo*Y|t6gNHeX zic^1rFgAFE2*M%`Y$BHutkEg0k-9sf0HF+vRdJUf+NakfgSwh18S?|Jjl~jdJSp~vTR+yrvA(+zFH}uj^+jhK}L>&x3=)IjS(l~4L3F2&P%e>PWFDCqN$)b*~7;64Gk z;Wk)$zPai2CbqpbtUYl~6}~s_?#^;bRGnscbGFdbAN!-c-cHvC?Qo6m-^>rMQLLqRE49w%R8JuJikK#I7R3lhmFZWp${G5MlbXdV-oL~v##>&KO zt_x@dJc^f@_<1Z)NF|6+fQ6cdH;FVD~e2!Z?Tex#z3cl<_zLp6N0Wa#IdIP!-vaGrzB)5UO@ z6~%vPcgYpft&3t0*`Q&MeoZ$Z`LdsnSjUb3IJ?dm609x*mE=V-?vJjfvvGF$ALN;x z*FUP3;ZtzWX<`hMnwt`cAk2gq~hyKe2{v!*B zVrtl-I;_3#)&}*kc$7%CTHxI@n)qz3$Kqep(ei)RYR+XDKBQc9;83!8m%+zVMZyOT@~L;I!$mt)dGZPfrv~AUi*U*jMyPrj z>eoLS`(5YUicuP#grj6jco?2s332{`*IYY+LEjxcbrh4`r#;2$StIc+_Ux>H$t)IMK zCu)6EtY$K8|X$YdmV~@&5 z^*V7}YYavToO4Z%K2UF6hvJ>^#U0(Tp6+5@Q4sNLS8*;1gKt2gChVoS^=fq=g2QEs zJ~`rba3X8gz{PGa_35PvQE_JtS=OxIkKKRNs4YzsNyz;}2E&TlTpps7J4LGY19d;O zbf503p6&-=tfBkqBk6wX>wa2U_tOXJeu{NJjp%;5zV4?F*ZtTa%XPo*APZy2p*K?M zfifJi*^k3~&%%Y`oBl7^PuJ5?c6fHIrrl@9tt6-Nfz~bU3P(u!=i;`kTwNpn%zFt7 z6=mB5es9M&lYIOJ54YFbgM=>w%&ZI()$DUV2%aN95o$onIRKBS1zV|kA@&_~DlM~Lpp z;oFI-K{ECiAtq{T23DHjf+)G{>_reX`z5dcgxrtwkm8{AsutZ-`EIrdn;0}Pm*qQG z{t)JPWFtrCOdKnCA(JN-Aqc%6&{sQg{#27t7B&y@Sx^z#(1ZwM=go~!;gge<7AFCx zlf4!o6XCng!^xJ4V_n_ZOh7aKEFstLlkgTPQ&Y#s6?|MMN;6ks{F&loFCMOTR`{uy z_bBmjClC))8uBNPhso?*c}&%*8dHUWgZgo9X~g`XK={#UFAeJ-DFFUMgjENlKxk7b z^bH3Z5iI_IlWZ3&Au;0U@W=yj4=l_)G4AO)xIZyYOx>qMSat-`gSU-Z(5?hr6()?66)(-Dey$<8(274TYW?KU_YVy zhA&@ui26Pw;&Cn9#|p;9+3?$wb{I+lnUld7DFQpslk6BB0c?{B87BgFkCQVQO;|s3 zXM3(hLV$(+m)wvd`g`g-QljS)j4yJ8Byf4i6)M;fDm|g}UDlAI2#*(>j@!bOdSu#t z>zuyOUGU*HcpxC~&`abHi9crD+Ie}Su#^zg;gAh(8Ml+z87cwLlLHzzf6bINp5A1W z>@xXj*1x&QW`$qEx7=oz3<+MCEuj#_iAMf#oTioVhwQCecda{8TaLQ40?R)wlr(Ok zBrNawW;VUeFST;1mB^MBUrWcKEz3|_mQuHz@VVv8C|a2K7UGfS1EXx7%_fWs7Dqng zRpzUkOt2#X)7*Z>_&%Oqe=bIFZPeu^g3aYNoKA{)a`w}AKcBJx|NZUH?S0moUtiFn ziaWYErHWHs+@p$n2KY8rzNO2%B={ZEKHa4%>>Bj8$R0Yli=Ax}NM~Eu+1}dfl5kQ? z%FfPCN)yyY{Oa^}db{229@%FXaW38K?QQR*dnCjj5>R_@Z>!VUe@$P{fJMF!#t}>7s_Bsq} zS}&No7`gY_>2BKHe`XNcd)?jMHiO5oXFzv)4CMB1+UfLY7Nv+soz50xPJ5T(0cdpg zwt8uIixIQC)o$-HwD#INyIb9KdvA~R!Fb+l!++hq9%Jopuif6+>vTIz%H6#HgSR?H zDLM@6on6)@-P`M>TYEbo`yEC}kAY{>VqGv+^*~lz@HfM1e~%Hx6tlav-Rbq1bQo!@ zd)9Avi*b+9+3xJ_FlF2AFjlm?J!TGj?RK}byS3ZdWoo+J-fA-fcDA~^yG(sLdp$-3 z>wUY|Wm?RtZnqg3OiLN=lk7L{cz8s|9M6&?&fU|Um`p9%WC|Oq+X^0jDR0*Cdh4cD z+A(+HwA=1ge`&Yf^YBb7(FgtswWQec5<4~m#Et{N=g>>bu~ArTIWT-~y|la)#k!6I z!{^*f%PUZ9?7Fo0TzqL;J;_sxC6j(NRdX9v)U++9Sw%(bIL#{RS=U9fs+#RM1N;}$ z(J14y&SLY`Y}Oay**KeDPgz)%Px`afY1W?&ui;jJfBt^bhdTUTfM2rJesb1gad^Sv z?gsnqteL!Ilg#OK)YOsYd@-98JVW!{4fJxzkac78Qx>GKz-rZK!1b_ANT2{v`PbbY zqk;vGt5(uK_fG^vBsQF%P3Qg5ceBfkNB7X$4)AB2r_*uvUn0FDqI<@f{-)Rq1xx7t zbNQX8e|{KoPWx}C6WN}XCC~GTz{Z*#jHa#RTHKcaPPpCDJ&3sWx9gm-eKciVU+0oV z`GmF1`^;@~fkELBD}{emW3ML0U^Kk|^v$R1T%ct);m87I)6r!E@lgfifc`k=_e?by z4lfuAaNmW#OC!G$GGYCI99Y#0e7Em4f7yb4f7QuKy@Suxy7wZyn3@4OG2w7Qar8+snY)kQ{<>fT!z3sk8$Bs5-ETu^15%9fhIsD-D~!=- zrO+GFJV}&JiqplQ2ss0vUjh}$m%}5i)AC^w!dMK^oTD3ztmeIEO!w%%XGspefA5(B zQmPt1Ou&UzAxtdWgfwI3n(YfkcA2A?*$!w!uIM1a)P#U#Zvzvsq#WO`uxDF(V88mw%fw)={@(EA%a!%H@eXmpo=k4D8L6^O`Nuz7 z$v=*5i(N5`UGbhbe}vGAJ5~M+e?YRYe6G@EZ9J=kWckd>@qP{e3ItAyQU;<$5LLAy z8aKw&JB+H1a{xoMFy{rrBIU8?;XfMBSv=mXAk^FvXnuh$Gxsc0d@0A`o9SdapHA|j z?ww5qAk#U2fLhU7gw*Vi>z$`ohoo9X(S|K0KI*W%)t}AzyynTs;9bbse^NDi0+D4T z8f5;SBabv%jsk36wUi?!OsiJs08Nd~L)vHZa+JM1`p=^Dz+Z(IAQYHP%g12Bl z%N+QX>On;d{B<4p$~j}Nf9S0E;unx%1sH%|L+uFSP2z0(G9S&enc^J9w*Qe+W6ZdJ z)MuPCiZ2U`QcftrSKuBev6W2iFlq|FO2z_*7_ceD;FZPTm4(R)VX_iD7Cc{>exOYi z#`CH^<86!kQVJkCnG0LvH_@rt6VJ>DBR8$t%u6ojHU( zh4{Cff{xXnaaP6DGsYllisel!?<9`mGEsr0yQRGs-9){W4?yX zHD&`;X2Y;=1IM=^WfK0KG5hCiC$h*>XbsbHsJXd|xsj4%7`lBbRA$0zv)70__ zYLFl?J^lBbouU}@e@$L|n6lWKv*k4ZNc$PWEOf*oIq>{B$$~o$SV*R+-Np;<9G-cb z_;6)sPoeZrN5(%1DB|}DvovDf_*a~FV-59Z-M{0c`%gIM{zIqSf881PzvYDcH2c*K z@xRPxg_vyXyUm#io!QRpZdvfRAvNJkc;(s~PTtI>H#9u)e@i*gj##6!!G7Ie4@3S9 z4(E}Gl2EJSxw+{9NA7_D9R!KC>`J6qGdTTou72l^Xi3}{&-;4CBtE(Hdu%1EQ15Nn zkncvavNw1;RBXiLA67bmbNl^bI$;KMQoJgP=`ineCm2Mam3(xN(UCFq*x;eUN71ju zfq!`BWoB>`e@4d_xdE@?Tkr6+O;65I$lMW>@x%zhF4)7@(-E zYudRTf7k)&EEU1$tSe8E5Rt_!WuZlj0p$_K9Xb`nTFdcGPa#ry$cWeGg@PQt_gU`2 zIh($cTW+wMH9Kq2o*XAN!v48#^zDy&$IH=?Z!GkosHJ@Sy)O}F+{z92`@ldJge7Nu z7`jLrL z-NGPrhg8@KT15?W7lY)BzU;u+wIcOK!-cBi4?O(A`1eWuaj*8Zkm%d($g>cBJARV` zYkX3)tCG)2I@DtZ^|&I*is!^LX*_xY0crRS-r*?q@BQN2>6--`1E8SrvA5&Ds1o^=RDOEuQC0yPg4b%@d)Kv(oqiP?8 zsu}oFYgmlsYFn^tp;8<~MZ0F!6t|8F$`det%J&6?y`E<*rH1l!4{@jzH*tSe1`0Ey zA-NT^pQ@(wpm9co)#rRtD&|rz%q*2K5sQtVbgg^V%rI4d)~y*n`XiW&Rm(pze;*K* z4>vaE`L(?bqAEzUWdm{C9o6fd(``%{LMQ|^>l^7oN(ZnSCQ7YxA@|2K!YZ|g9X%{K z*!2?YCeE7b6`Z&`%BAZ(&nI>xbo#H%9L#+O5~^FzHv6?8#{?FQx5z~8Ww!k8>hP>_ zbkwxR^;;II!h!<%lHP6NFB#%Ne?x>EjQh8gN;px^2Q+NLD3gl?N<_hRA2DW%cI@Bs zodcD)qF~v)5sH6nmT(ChL5zYW{f1fS4|A073TS&<0w7YF@}*FVUzo=Sf1C>&m<=2l z`y>c>0S~hB-ZeHMp@1g;nN$?of53rVP)T(H(&MZuaaoIKZP+=?63s;o|8&}GKm^$K zDEb>_HrG5=>}j*dxq6J3dmKWkKDlLz96JMvzdN;BXz7TX=s;VT^pw%b-2i;p)>Js@ zk8)@LhGU0j0Sprl8kjLof55sKODLz73taZ`)xMac3UaZtpZ7mP>*d@CGtLW`Hlr`!97MdF%G$SRaqwEcRH z+&WLggDDY^;?;WnEUnU_xux&rJrD>^w#2-3;r-025WIN14F_3eQ_5qI4p zV^gn#8e==hLl!VaUJ?wWPaBf?x-dTa++-pfcPme{LW*1uJ;AK099Bo>kfzHmaTL^3 z(>ucu*vNy!C(VG7&eOL`cyKES2O1i;3VSt5hxb8!%x?}~wUXCHH5%||lj{fk`3jbU z*w5FK2q`3g&ROeof6p#B@&>c!K~ro^0`T^nkQL);@MfC<8dzWAdiO6+0tLRnJmOgMv+p{x2v96MZz{_V`~c7^=XYLD(rqKFO8ikGbv{$);n+M`HhsC7y5k z^XpB~*E!gX{I#Q=5b{!LeHKTFB@>G`##YpxlMgBw1RKcCag!@59#b4&&rNVvCLUJa zG99I-`Q+*Kl=smDN95?KEcjjYl=mg{G@r!vG@m?$p7LI$jxbh8;!EpP)l=Cnpr8(5 zUqM-gr&Lgjr9lOCPu2bEy3tm0HItkw8-GGDT00H18KvMD$c-ha!GTkQwS`ImLVU3I zJnN*t%YjBX!urEM7ItN*W zCtE^P#tRDWXm*q-!K=rY?C%C zB1ztkfu&3Ncj94T*7!^v-GT8qZ8Z~ZUmV2hb@aYL#8AgBve zaTX+9Wh4>-PotA|f8N@>`kin)cFPBop({FnaiE0F!B?|alS{kxt6BDzjbpd{Q8uCU zF68q9sulBd^;ICuh>(HN>QbEp^d=la8!BKBs;R!4jRY0YmcgJsy(b~m-Mv5&x2&O3 zVrT7F*=as`Kg#4ja`BP$V|j2pbxy8m`C7prfV<$%T3n4t8!Gmg}XcwY+K-e zzRtc`j7Um9P?UzV_;*gePwd(QBKZn_Iag%(nS918SGB_cMIJ*wxSOeb9B>1Hk6Ahe ztSZc}`!|PYt>oQt;|ex9|IcyqP90WOIs6%a3qX8%7r01*UL*0-srb$alfyIjM&xjB zgaKt=8o?X*V)HJS;Pw0qChi0wm6Mf!qI#GXT@C=R3_W#2ne!_#@#mZAm^>O+t;7wn zY03SR&#&K!ml{BZt>i5dqxjB0h9vsVyz=nw7%GN@yS^;f6_!9zzat@5gyl!RLBT8& znjH-xL}f1q8f$`KIWiOwy3SG<)z@8=`|eVHk|hS`Vm3+SuO zWWvqK!l&?bK6X*R@M&L2_d1&~c|V=&GiV`i<|(3!Fxjf%>#xi2Iy8HKp3%FDz7>}n3n%)(8=3bVLU{T1BJkTb{l%JG=5N*x5Wb6te$3UIt?K#i7=bFshW>sb870h6tA%B%gdE{ce})~l|hd98-Nd~(Z7;dM)H@X>E1 zz)dSRqJ(cH!EYxB`qlcCWj3%yXt1BKR)Y=p17BM+xor%%^pkxVcc#xrK z=WRB)S`q0Ti!i?Xr7ki2?o0lae|oKOH`I7Hf9fuwGY*#?${9g_eV|?v*9YZ-pG~K_ zWQ)6G4xh2)2hz6AFRFMBy*)9u&h7gEv<{GXEY|cgN+dC^?Uv__0NA_y{WW&OXNvuf z_mwVr?Q!HvZH&;Jq7hkuclSvU0|{?fHj-cxYL6rcHE!1uH8qr=Vuuu6l~f5)?MWiI zidY$MRw9Z(`>FtcFxUP_FC7qMJvS|_BjBf%i+%06Ht=hY=BGiZ1II%zxf7y1v~uaZ zH0-Cf-M_9+jd0Z3cUN}QLL_ld4V!3{r|xqiuf)b$!c)U$+=1_@JtGhdtYnuD_tlO{ zX}5ct&Eb&9uctTJ5ON!Zx~U|#ZCoD;D7-TQ*b8%{Ki$WFC;Rrbe#LIBLpW95TLtPqZ{eY!UmBA+eN;GqsaL!nk) z5jxMXPqH}!t(BMHz3m@~pXd%*g*NvsjF051mw2k`he`hHB6~VJkqGMiKK-KWMwp4sDvFM-9-44$#mqYwiQ@d1>ajK6Z&Fymgf}ydrC)Yh;(OF4-`BwlFa93?r6@J3)lS%2_sC%nJ7R zy$e_9$<^G9U>vylGp0nPniG&R=S!uUf*TK1M=Zcc)l2~F&zN~XT0wb5{>iTi?X8Nq zOO7_5neoD^9c67-3(;3Y;GhyVF;9>05 z099RFShIK6vdigI?4b!&>=Qjk2~{KtKLIo<&=*R51eJC{&0dLVT#P(0(1|SPhg1vO zHUZ|MKdKsbq9zQKd&iZ^W8B?g*t&n#0@Sd~9A&eJS!oQ;6=-0jeHHIR9`S?&JkdLU zqT_Eep(mMshZmVVEckW&QA`l9WF@xZEbsU-ru%vabY?0X$r>i|7t=3m_LRZwNf2RW zEDdsvCCs0)dxn?zrR-SFoQpf3uPQQFGs!ymD$l*TBp#`%W)C|&AZ(L)gvfNJ9pyAD z>}%1@cUaEl;|ey}8Qja^QVbYo_ZDq`lH^WETT~YT?uv^b27YGX(;$i=cr-sLsXln^jSphO<@NK0jB6psYlHngPzw z(s}}O2>!;lpFriv*k}e)D}^IEk+)j9vtLD6eA@bUIiK~1{POK@8J_a?T0gZ$=(4~jd-cWd8JRiHn)<$|I>c3 zj~u%m^M$?$2I=w~Eh7VP-< zVnZegt<<4-(2f_0m#H|(meZ4BW1`vs8L@w^s+_ZSo?|oub>FTsVt;y3Kkj3UB_cA9 z1x6ofbeJsGxfF|6)D7Wcr;e~C+JwBv8|!j*z1JGUhEV0@Mf%}I=Z+tLyps_HOq^}l zI98N#tiU*AcR}M=g^gonTZWNCP2+GM-Nd2_naBTsPi_V!UuIs`Q=Gn}Dp(kLRxD&- zo{#29e08$vE>h~a@l{b4-BW4{4JElIT;jSsqf}V}no+uJRxW0Mh@XKeU=)38w%`Inci`0Y)mRJ zV*+a1uE7kw%Xw19jEN>%)6s4v6DrHZ@r88+Ifpmsy6@SPZ^#yZ_l2OVL%26IGAvaF znU1jK#uMd0gIqe1asinf;8~lOc;Sui-LFeHnwFUvtm)k};su}3^hcQ$V8?49FNiZB zEm3M#VGyUkVp=)RiuuVH-hwE;=`Ztfe`Gerd#hEgWZYkx>>iO3IVluSSTJI>b@t9Y z|0MgdD^Q7pud}{?K`x(^BbQG~kmC?}$N7Z9Omt#bpfHmpnB&Nb>IX3|y3j{*R!!F{ zvs6-O5a%3u5LZjEc3G}buF7kn1%=wv5WzHr;rIR7JP+e2t(9ZJ{((n-3A9_^h?J-wnd^lzJ z(dyQcAgfJPh3}3K?Ipf1Wgs41{j-<*-mE75aX#cv=rN+bb}|?~nal~Gc(E~CLWxuW z*lJoN7&b4snN4r=OD1sywPjV?%;(wI{Wk31^oRL>eC2$8m)*>qPe1lY`Q?8(9}5lj0V#gycG#lyRbCw1U!qQpDfh(@nu*X zANHkfe1QatKLV-hG09ix)Bu;ozAcLb%nLn#KYs-q(J!;5zPURS8!6z7i5iscgwZ9K?VLtQ}6(!DQOI{3Dr4pH4CvBgE}BsE8G-p@XBU? zx7np+@MU(@UySDb!3>JaF-}(F;2OMHO9qNC%gwwr>Ve03W>{Y!!&B82d&ORS4e;2i z{}O8)-k^^w9UGvsrb%Hsoxc$h_||-Fpc>voT`aD#Ix@7H9^SD*c{Ck1uy9*R7^-7~ zVw7u?>4N^wC48)XqSlfB7UOXpa}(o#gv-02D(M$eXfF-*)ZgW52RBv8(MLU#V8o^z zH~;z49CCIn(FQ@8p$aWx9y!Wrk2`DF)Fl~U1l!6{Ee#5OXT5IV7~Ry=C)eR<59G_ z7)#DB1a-zWI&rzeM0}xEknJRl&f9R1{;_Piy(qBHDYRW9uxZKOnj~m{P;EM`WSOE( zomY*ec$S6zlG?|vm;CjaW%?|z`}B+Hc)XbRIo@Xq?;p@c6q8o`AwU6a>2!#I&6v*Z zU@J(hRiI5mGn8>yoHhl5B;-|5OozEeh=aeI_e4Fml8@C$_~?FH!nbN*vZhg2ibo3L@5%w~_&-}7o6p037h7@Ot8b-J@%0Pb*qC6|Tux427~%=4#1 zL?=0IWNhzi?Y8$_){`NJk$6sXODrrI98L;{UvXs2h;2aV2I2-t3!W)^<}FcTBrH{Z zFbW77jetKMP9|&^&n_P>5`GwIWr@O((%oG}O+KB^rjz%h)gxlJE-GiU{-ns~YkCqh z*48kpkIf(xKZfyt#7miVP<`hsj6y4*(5l$5#xL_EXsKgJ==pHIHXWquKLRB+DENMs zJ+cHS#Dcxs8)2RhgA%TW5Y)S?hM5W$9tp{sq78-(h1~Xa+=!gbg@e0&e45ujy~YdG zc`rMx&6W48O1U^o`_LO9Ce5-eHdkI`FyYOu`!0kSwwg4q&SLc@Dm zF+_waUyIjE13$)YweO^i-J)KQ-J-Z2yJaIDV+CoDmBKz19Yc>&VBfN04PtpK`GBwB z{(#>1ps*^`li?pOs7c)qlYBV6gsm*(_s!RRxzB~Kl_!5c`ReaKpZ@Uf-FIKTI(z%` zHz(ijGnagSnSDQngwOs_vbB}&Z3nBr`iEP6yW82*)xZAkr#SHKZrTpj_F?aIdtF`o z)#>TUSKq#U^Yiy#zxwv=sZfi-?JmDa>r=Z0yVcWH(q+H&*neB>zilo=v0L3z#FGh| z@8|C)+2!}6{v>PUsAnTE$l~5WIrPxTljCCsvI)6=E7q;Z_lRPqZw_`!f#$253=wq% z_oEMP(;jbZl;9}obUHoupKkN_{QdRmVm6z;XBcAuHwaY;#g{2Syn%mw`SCWtCRsMWCVgItA1{na275cZSrZg}*669$$2N}oh;a|R$-o8L|+*?(D8)%khE zlq1EJdQ6e&hxv@DHDfmJ_H;USy7fvE+?M+$UMThqn!57bcB6S99?})H?iA9jt!&50 z=Zn^|!bM2_3cwmlfJM%AIzyJ-xZTHw&V{<4#AIj#e3JpdO8At)WnDYSSfU_M7dIz= z`RDvthh=IF_n%qn%;Jtt96?qiEn|(C+o}r?;fjUCIZ-}N%}1?eJi$LseS2*scjFHK zH??2DWM7%PfX{kuq$c%14iK#tuE>iI1qtKy!28S*P6l|@n&AcY;k)^0-=kqSARvM* zFxsqpddbLOwcQt+5$>f&xUa$s#H`(N}OhtJh?8#eSCsfm&j`{sUKsI=m#@LQ| z#9j(s=fHe4E{2~+tJ|Zx-$60m^KM8yvQ9;3Bevd*@9@3gNhJqqA;h(<{8nE&%L@J@l_OiAZu{b)d4Bgm$k98UmJ&dhT)l*xz8IBwz-ztT)W zl5vcT39E{LJy6QJWmjOlv^>|fy(vY_BdFBvKJk^&XzR|7Lyl;!qE?j5#v<2rZ>EsEVpE$2x}f zL0zV&VO$tW51zToB)-@27~m>`vCWO}7o~dW3@XSaa0uE52sT%dsrDblc&XbzN(g76 zUW(e-41VWh^wh;;4CMUr3?WnZO=CIQD#cl6*giLxBb#VOk6}u&#_oQ9z1m$_-pr+= z0)G!M$&AM(sH+;>!;UXJ^p&KXlTm11OsYkN*>H7bRt_<6RyD392*1;{bUI4m*iqq{ zwnd)XmkRwD*2$yS2h)fz#e4vrk7eZr$u;RQtAH#T)oj=5CqS)dU>2ya$BrTh@R3qR!7c%9;~x~=FI0}awQtV zp{!c-gsUmsI|Em{-!i+toc=bMPl>4k>VQW)F;1N4dV4GeQK*KBMg-H}_CCp$^Y~x@ zND~<~{#vQBc#Jj>4NxIKK;PGP4ggDeZ!H@5Xc8WNd?AvJwW4lPb1laZPTUzLEY{ z;*N@bky%UXYB)LKURHfM)^+H?=g3K8^H1N^OS*7;iDOs>5+O{)Klg@AY3ocEXNrLDyn zu8iz2^Xd5BU;)qxFZO6EYMk{r=n#~PBZ8)mdLXI-9kR}GfFKf{W|@<4@nv&TfYchr z?Y@8?T++A2e{~`@oE5i{x&vLV1a!hV$v4LV6|gm}hf5^u?Aa#)*e1_`Dn1;Gjc;^S z*luT4g&lSNR2sPODyF+We>CP{y;t!J5JNQgQQ%(02SkcTAf~a1$X24EnF>E-+k4+@ zR~_B3b~p`9>KDsajl))q7-GDcaEiu1%&&GW0Pq2CfBV`b<1o~#1@84~o>_Pd7u?G) z(2(eKsvp@K16U5=;bUe64h{A2rm&FbHHc5%EM_T`n0!2e(Q4Wf z9jldM+1BS#&Dg-xGt~5H6peM@Xj*6c2~`au3b)@n%2p%hsH<)c-4*oBY4JxYoQ#pw zJV^fOf7*myWTPJnrrdfufcoM0*p6yeDAcPzD7|2o_K!t3ce^+4=<9_F&S%r3fPBYjH`rnPvf6k5273q;%`&=(}3|@>wsj8P=O4aDA?b?pP zwKA%0nn+xCr_njAAi?2;tn^ATiT!8YCnQe_An5P1hZ<~dPI1&1#e9467n$c ze{~2=oXkrpskSkWiMP`#DA73L*Z3?+wGdA1Tvxa#=Llxt133Z&Z)@_^ktc!yX^;T{ zRd*Nw*V`N=joajJNvEB5<(aKc+xYioN7vZyZFN$9xT`HIZlhRGS4-R7&URBa|HT+22XNsdML5DH60wF%E znsQ-C+g5Ta*4q+VV1m)^M7PY7!KeM%C?7N1=%nrT{hFeE9Ff=_soasp$Dvvhf3OXI ztV2=c=uj2Q5m)2zgn0K)Iv*xyvcZY*?>&?K zYtFwB*433E&d#c|MBS#$UoXsemR?TQXjk?IQVqu56Wz) zS?+@}96q^bSTSX4Sn2HbJO-p`S8)f{k9BTCGia|9Wl+dy>M^MMu+)#o$N04Qp?u`~ zrmyoEDoSNhqha8I;L{%9*4b{8oaMJ`HPUp;7YhqQpkY8HqM_YYcPHFpe``;6)!ik! z+KYD8bo9eeUO_z~-l?93^nOa9y((F5K^{Y z$Jc;fx304Fdf^tmZmG^V#fZRwPW?g2)W2}*4}tEwpyS$1g6`6wdoJjR!80hm0QBA; zl(W2*F+hc^BxonjO6ulmf4diNF9aEEU!E2f;&K6mYHJCY29+|SqWYs{Mnz=x=n2rJ zN&lrga$>sUq~nyQT!s>8P@!^uG{6_?(gw{2>DRP=*qoq(!b;Pp04MZhA7wXJhEIFD zJv_Qsc%o@o+J)9H0y#v>?OFacon%pt7EpJjDu1H1>%H$F;a+`!9R( zWMx)5c!j?uU1}9$iI!MoJ#XQpu`=to)mODT%t_Z;*TOdTe>hUHL!Oc_DL&_TG`Uy< z#@I@7eDp-t*&;-?svt5WTGJm@sTfRrF?a39VO`1Q~}2wK8_aHk8yG z0TYvmX#ZY+1L$v1b~1sw%1RTB@u|?iu_)XSv9M{~1%SHM{-ewN2gd@zIHkE_b!qBY zTohdnG3$_vZcyy%e(ITwL>JZop%}t+!e>fDP!a)43Z-FR1w}=lcKC65V zlG?h@4ROE|=osoIKXBuiq(a0tz;Cnc^6>3(1H4o&o`4W{(r2^Tbhe+o1=~&i?!%Pd&!#thxT{CGq)~{|7!I?de^9ySAaY8uT3IL@rCK^jny>4j2&!9- zTnsbjH4eZ00$x}7joF@7FQ(ZqkCQLIU^ssHg@v1_2(dt+AiCxuS^wf)D|zu2Ohj{1 zn8!O9w=J##H!7Qq{94Ou8Z)gCKY&IwH8oQ0Euc6>6Olc=^Xy5`zNSgN(;!Q9 ze?xM(u!L__(G0I)Swb6-+j&<>QAuRPqF1vVC85M|J8IN69ugw~KGS#ZIcgdJr`J{ef0@VMI(o09t?|K%whl^C>ZMp2MW{A@X!bvb z_Mb`R*5I`Pv=S@qFr$4{V+b)sg00FHNsX}t{-b~ggokznTPu7$R6~>^A{4w@KFoS@ z+#mS^MyiHuZK@m6RyWo(){R<2Gai;*lPw7Wh=Ex=C-wgTP)h*<6ay3h000O817miC hlbudD4r6wNR~J$P#(hly007#P<4!9Ebxr^P003c65I6t; delta 18950 zcmV(?K-a(fodJ}d0S!<~0|XQR000O8_l9th4bXr0hHzKzYTY%KO#lE9+W`Ov0001R za&KpHVQuYwX>%Jnvfy|Bit>wiBeG3v$Rc$gFXXm+MzMXZrS3Ttihd+jvdYav%_7yL zE$we#B+dkoKvhvvA8&VJ+L8)DB5x!T*I)mdT=lOftE9Kt-E42RU;Op23H&#|$$q+> zO+SCk`r{WbUW}(#i&2)mg_>vctFQAxv3WAf=QrbQo)0(Q=69!)c{ZE$N5!|($ta&> z{aNz)MUsrN@wlIS4ga!A-(9yGSNlmmnKxNklFYJS7WphIlB?w9QPSq$vPrRkPwj+Z zmK=%C0P5j|2k*`5EE`={26?4Gb^;*J#{GZMh{0_%t#;Sb8T+0rTdeix{rN2a@FANe zOMv!}?C&#F50BWNhphN7e_{U|voA+S$D&4zg!fq=y8GL_vD{~v_eZT{C4O;;Su&U_ z`_l@#*|Z6S4&i$z=@%S~?)RZohTlxD%4NtZeRuuuY&JbD;NQlW;yhzVGInJ7pUHnX z#)z*LldJwXo6I>sSTDd32AOfZqHLD{{wnz*X>hJLlUMB1e4{fyEW*U4>T4P3i*@t9KlzYp-jUMb$UD;E z>I=|CpOsZ+F{+?4i_sZl;cz}$eLsIK@_Bw|5L_Vy5jG4NW=HVLN^%)KeZeh&Bz!Sq z-G2gwj6vogxaKf|xq0&6SywBiPXXws#Ys_2hk2jCzLk6m^wn6ge?B$2$avT6uUH>% z^MWyIuz*fZuCD6z^UCVy75^FO>$}-iHUrJ4*oCxGTN&~?{x_*VUq}ySv-^MeNJvxv z6%nG)lhX+U+#luhRg?pk@i@Nmlc(dHAzYy_V*)Dvre9>+Jzi&e+y7;eCAYKeDj)Xe zS#ny4(l2lNv&L{g8M2>E2{1{9AcT!q8_E5>{Qa-|_l@=jFlh+?Z0w0oC+O3^#iu^{ z^l8IplIixe*m;xBap#D18$W+rSs37?lkURc04+7vv+RzI6?W6+f$E-M!4H$${?%1> zCF+CNm@XCjNx^?J?6@!PnOo^`2g#Ixf0OR@XKZJ;KS}cIBnRxbyATjfBzk{Lr~>e)$V`>g zs`ARNvXz2RbNFYwgDW=j9%gPWi`rGb!O^29j`4>YkLdTLRy6wsOUG0 z40F%od(&qnDwdqAq+?pHP<%e+V6-fmSZ&NAI$tW-Frtj_+Hw)gx4V{Tw4viFsa3_b zc`WoH6G=}=gbSb3Ww(E~y@AvIH4;1l09Q1!w<;nn_`E+G<>P#wr0sV5f&FndGNe&R>BM!;25h zVMPVFhG1e8bLoF|W0E&NroHp&S@sJ|O9ppo4>YP9QvO%2=48W<-26e#Et(X4PKYj{v-9vIwAL(@Yca4THg92`P8NA!@Z zZb%uq!w9KkFQSfI&$hcJP7LT{Cyi80QN`^@y{^_=zXDQS_Fp%szKRXD4omvWwYV42 z;$2dUfpUNTIki4-3+3)cmD@+w*KntfE9`)-JFO_C(lA`Dx7(tMg|AGm1@s6D(CrN!Yh_K-*k zDGO8xE>(4JxT!@~K&-fqEmI7siTnY$15CjIL85;w9LPe~W4pR7x+26-U8!+ni+xW@ zx2IDFw$eFthix`&A<;RK!0mlDT+E96E*q_UBN{~YMWy+8$yGL-Wh_+VMVdh@s+SyY z<7CFgrQo;8T3Bqp*xc-0!g3CQ;ze(B^O7riGFTZ-B|r z`(J+7pl7$jm(0Q`C$(nz^N|?M=b%noGF|%CCCX z%<^C;qJj_neXO z{!^GoRp?@&S2-@%+Xrkr%7jYe5Xpl^kfUtIug4OKl!N4ca4*(7fgC(Y4VdJ*mtrsz z+M>5-VyC}}Sq7b_1 z)*HJ9pyXZf>7lWUQ&VyD8dM&=eAIs{j$Yl;(Q81DUOhE>b)RVTqPQO!y}I7$)gwnQ zTh!WNcYm|d3svZ%3SDKTnq4h%(9 z5P~Ab13~BlHM|wk;mrdjy<;R$9)yM;0xdbX8N092f*v}9(B%~QW8D0bck|Zr+skv}SF!NDCqlMl&6cs9Rv?&^dC>n5z@M8GDqDc5i zUo?swAN$7$gy0vY6@m0S(b~?!6R>23z}AKXpAB{g1`wf|m@20>r5G~sdP1r~TUUbX z1j7E+7T=Kh5%FkfUod~MJBq9r8ps0Tr$%rM*Ge=}iWx)JOA8uiRLVG7)xA`b<>7Tz zcVA>3`O6EK8 zdgEvVGNvkIiR`$1u&qTi*EOTmDhTSyqtiP`B2{ubR&_MfAaXRWK;prEm_o6Ca19Cr z4$C9N8w=LKzmk8O45U^_$5fHXuvyb=)Y%r@sm~85&k_Q}3#}PgDP++`$KWQ!k8<9G z^-c#>J#A^f^uSj|>Mm|2F+ydG!zjmsy=b;6jA*18fk4^#XL=ftSw%dVqeD7J_uZsM z&48&v$6=m{G`vX3O?iX>RS%P3NW1pb;;bYpvW%=0>2-gV{UO#tdF<=~B4`ei!rI?klOJ-rSPe(qS%Wo)~uCWv6{hs%tCK9M)hV*k~}*DM6U!E#1`<( zUCh21aD)d8VMGRX(j>bmDelCJQ_UlseaZxz?N1&56K6BiCe78rR#%d(71&sfIRU-N zc(sgI15{;YtPEtTr`G<_dPg0eWV^VnsmO|IG8ccfbd^6mr$u!R>gunWOady8Q#WGz z>7Zv#K%doch*NEj_pOR-Oao)57h~raqe>N1)CWwQ<=n}+KgIZfM_5;18)3!Q^Sp>g zlk+?pSY5@|He!uco`yT4l&9{|@|2gW%}cz;4c;Z?<|4ysfydenuXH0k(~a=9S{&=^ z`vZU7!Q-4m#VJ7;8$3b;VG##5kxL2I=#jTxV6?<>1;VTzr^LajaD;1*)qAG{YzB|E@T-k# z5S&3T7J8vlFZ@Df-pGbkiVVX%!2YPIM@D~cnV_zr!_QnB$#$KRcAY@Gw4_~n>1V+% z;^?(X(1?|bfywABAz}ZlcVW9qszRr%0^uktOwrSj=X$y+y2n2@73^#~Gx1c-#A{E^ zX$ndv=V`zd%Sfy9!gIDM;cVBPoVVS{c*!(8r9#9?)9{W>-IGki+fOzJuQ(&aS3az4+dkCN<&Av1H%m#g0m`WpszElYCpj&s{NQLlvd;5q$$Fb z$7;UQfpEr;w&(w0)1@byhB%^rhPg(KsYKc3tM#@LQf7FaPx>P+#j}(D4;4AFx#{#K zw!Jm1J#kJIzBlgv-f~J*oo0A*w$Ric`=h+xPS;26aEW|*I-C!_VCw}_i^wYkIyfg1|b=SWkBx~KM&PuPr1D< zg*Nc_ane!d=JC2d*p30)7GPh}=)SDgUE%lC#ss)Vh^19$-%y!(YEgf#W{RlRql7Nu zAP1okct8f`@!1ScGKoiV9WAO6EU=gRtO|b4e>FO+;4x0HgmGhKVm8+Wv;rQ*%S>|n zTr!Wb@`~hLZ}3Cxw(WAQS>3xP;BtZ7f+i88$oXb^)osXbTF^lYAe*s0<_15n!4wzB zlQ9Jw@NdHuPf3x#MIPQKgZ2fLkfu)Xk*7mB3F-llpXJX9^^nKU$)RB61TX@&0{4Hm ze@2RlLipzw=p}@}eRe-mQOSFLBf+5>zFIQ$b50!j!x%Wv!RFawILwOTzqGsL3hCBG zv4?EXut&e98<2d}&qu7|#($jOWDE&bmw`(1A{qBb*VEZJyZR6E%+8x1Rm<=xxR*3B zhDps$3B-_P&qaRpPdt6NnHF;tQVZDff1+_BpvK1=B+Wzr`)!n-gj$* zdR#n8BwH=;ZW>K|w$@~6LP86&rO1ab(+(Z#sDN-E{5#fg2@%EL)n; zmTfsmWYp2aK;DMpfw6W6sP!%da>~c7hz6$mVu24-M8|#P#*z+mXeo7$3Abo@e`_@t zvJ4+mE;?{1*}Ti(ROC=p#h2lVa1mQ|<*j%g*4uHEZBv zx0m|#+JvaMvxY2d*6+t|e`?g0rimov;W2|@MQtt*QOcbnRr`^;pIW+4cU4dK12ERm z{q%`+KlOD#t*ra$BXvK;x}QdLKV4t<)5q(6Y>?%;Uw4p&G33x2DfK`Zj@azSVZLYK zLh()i=j_8i3r7^N`}8^{N)#Q~7ST2%8u*F_+~#SAG|h z6&5TAgCEdWJ8}M8lSvjf59wJ@5!uj$2xI5XjZopUla3ZA0q2vp79bPxyUxSOmWpFt z-Pue)GyW(c*Kd>Q7AaG6$Hx_XTqsI2S7H2-;$tr!u69=VxtRAP@o*;)4^tZQ2akuz z>|A+F)u|d&g@S|nac*hE{HQ?q$!ISP>z^n9{#}Gs2ctk}Qz`Tf2O1G9eutA~7b_t% z;^^?mBXAEa%seyh={mSSGfw2Gx-d?*^>~XN;T<`Tld%^Z0ZNn37c~JIlLQzqJd)}{ zU{OVV)3Ew>Dywf=qQ0dkEB+Mf>s~4FOzIn0I9OYKL-$}mqxyy~UwDlAz98apE!?LH z#>Lt2yOVDiN&%gdx)>=SyU2NRcmY5AMZ%zJN%1Fo7ojJ57yOA{)Gm0V6{F&OlLHwi z0{4KEEE!E$zi?-Ju0%qBh5eV@kRtkf?mJSV=Ms!Ba)cysdCV0m*byo{q4ZtWkfI2W z7o3i}!j*bt+I{DozR+Fp;Wl_6An?#j{yf9lrA&L`?{NXrFE8!2>Tet37cciu) zb!i2be_AMM+(JoM-t+BjdY4~mCSGSp9M*^m~{etm*JiUKfjI!iy|9Y}In_qpM4~k9H2^ZjSIw|JK z`9Hq<>74!l@9%zU?=vv`9)k{5+|k7;Rh;VL9#z~kz_+RLEnVIv!S9&%=`K}a*PypW z_Rzsy>}-=jI@`L=_SROHgp*=Yc6N4BnxHP?SEskr+wE@m$UeJ>bLn1hZ+j=*BO!nG zkbv5Idt05(cFOvv>mqjSLic+++dG~1HqDwXL-tPE-rCvP>$ST(d+E*|&4TT&uD_S2 z-7ag?-QL~m?d)vrwn-wl5z}^iz3rV|uf5aVY42@qb+%~+c2Xqsopz_!>FjoU+wI== zUfS*KbUWL-J6(omXKQ!2*I`)Gdcl9x#mK$aPIuGpHiOXK>+bfp89atP1G>{=Ah&nZ zPNzq+C`CN#bha3C+Pe%7K%=v_)l0iujF{c6c6*nhwb$O+-Rh>>dwZ-8#`9hq{_F1b z7;ATX?e@-Ir`ust?(PK`ywx#E(P3Ec?6NlL-d-==+S>uy?=VVw3_Oz->w}~!x4WI)t=-Np zQ`7DCR+|y9v(??*W$M$}>oFo&@7ujD(_&V2yUoa8TFP*rWWRC`#6vsgftDO`?x*g> ztZK<-RoGD7R`3E$d9#k!TQ`5L(vGk1O1tfzhi6)eKJZVdCB>H4*s&2Hb{qgc zhhAHbjlyEff#GxOwdJiS)^!{hKIdLrUV&m`*QLeh;%nRLNuF9Pne?lvn%k(NrfoUR zDk@sXX;x9sx-ODc)odp;(tkM}jWRwDEjCYPv;Im9_~UGTGi8xhKIwnYR%cm%HoSq0 z0{Z(&A1d*y0)Ea``^kBWh2{kd#T)Fm^Jemz%{!;lQBwz>^TljZ@TARmx6sWYL)#74 z&sf~TVy#u90XN1rA*TXB2O~`kQ}Zdlamy_b=pko(*EeIqkolPGoylmb}a-0vl_>Fq*cK8*zmK zxZ`$9_aH*uUvF|IfYFq7eUnQT`eIJ{ygz!ez!dX4;A$b|I+a$tW|FY$H1H~g^+_EqOE z^|}skCR%W%!Od7tq8aP3<1{t3gcc9~I@>`Nzq{+7)T|Jh3Zb=(*;D`w^5uND~fKbzWU{$F~ENi#Sd{+tnT~szDPwqFb0gLciI2SRz(0AX5e`NsPfd*cmo&Ph9+~Z zO9q`8=7$d%Q>zVz*aIYACE`q7mt0ww{L)$Z86I&HbwN#mm@>e!9Rj_9;Nfm8NaKx7 zAeHwbetRvdNCq>?Si^e?Th@_8tRh3B!i_SL(}E<^7`K183_dR(XpV0kk-$0xZ z-z9%HE^V4~Msu!d&f$puQc#>%p}63V_|XbP(T&8^49JNIhYO0MPm0N0k^JtL1sg0T zLGjq=Npb0Z8$uh9VvIM$vmjVuj7BSk-jL==qI6oEEe1u%8TkAXs7SsX9%-GH@0Sq9 zVuxUn#Q79L3CbKpS%5 z2MMMo1T1?Sn1Ch4!!Znr+%V{L@)3rJyNqIzcXKz3ifmhFUABZh+tLI3)h}Zv26OfI zhA&^PtS^mshzs^~a+l3Wm2JvD{?$tUd2Czkidlc`iub(vBZOPrsq)tXl6~cKl`d=J zSsf(H7gj3xYxq|na9Wfy5UrJ{stwV&F{YktRCSzl8lr_cRuC2`k4F#x*?7sK^=1X3 z=9WP7OKh3BXPM$lITqhcC)4?Kk`Hz7Y@z@O(fK3Piq;~eW`|twJheI`)hdcM>^$*N zhgE;D{%p=?JhbPOY3cz2eN&nOE4;ivO|G(y{t8&Z?Mt#u!9RyS%C9y~I)6Ln^Se zw^|`xVwJ_Fnlaxj?o@k8)w4Xnm@j{GjoAQ|*)Z(eKy%ZjddE_(JyUFCgorvO8m}~k zT}RU@&tIQ(`s&Q7e(%X^2%SIZ)U|(n(i$X4Oj-YD&R9`2`Zg~aYDqWuhE z7CLs39C-PXWWhZLEF{y^ZsQeq4llg@f4H)<9Z~wHBjcY06!Ck7nHw>e{4>tQv4;9H z@!xPF{s)|g|E|;UKkqF3fA%CCR(kAU|EqjfhzYp9Ae|Z0x$V~Omj!=dQnPzr^8QEt4xV&IxS+pdL$3hSg z=ED#Q!2^$DR!YE^Naj3!RD`iPmXaeDKj``apFn)c3M!c z8nDkG?WH?|0SZ|eT;srgXTQmX^Prx+W4~vUIk?HQQ9ks9y(~7&AANuBG5N#Y{AU0; zz89bm{|Gb(oGS`fU2Q2g{xUrK$>wG%MF*zjSE>Wse?Z+10-^~zPl#L zD>{;tO#M=%>PxD}2bZ>j?;^@NG+m-f%B!TZ;%nB%l@x=*$j&;K7pyY;mMUW8Lxk{= z|H?|NIC9p3KoWy6Tf2W}{29bq#{flTUDM9(zz#)csR%=7U3nCRh%sg<3o=>^D33Mn z(a|E-T8?yjGLg!YO1w5N6y)d))N0mhu7lzC@UDD>vNl0|Qw&mYnlp=rU=LXRA1nW6{<`dSri6>@1^(tGO7i)H$v> z%!JR)e4BFI{n-^fSf0;UOxHc2_JoCZ3xm)-Qei866*bI-4w5hW#sp`di_{wp7pjUs z@bCxY-)Hs5gW3s0qHnh&4^;T=_;nDh@oCYnN&hZ3ymZzUJ`Gu@#qNzq~SYw zhvU`1_ls|*Zx?@T41j{d$KH#-UQ&#QjwnD9nt8uQsvyml4a9NxRIm3=w=rc1p%B!p zZ=?q)9l&asD7D^&+#k;kt0W(G^sw|`*GsJHJZq{~aN_PLm#*_NpV*Di5yCQaFqbAs zsBS&m?AL-E6Ie9fB2%_k+48&V!}G?`QPUpR?^u7R3QG&*b9{G+zj%lT4H0rM?%z== z;Y2+j(Xa`lOfHrx`RMjifG{iBJU9cucr{z5YRn=wSdpZyArn`OqS#`KtSy(%Bm9^W z#|ShFu9KM>sKb_k{Vl18r;4Q${Cu1Mp$1Q{kjP%AtP&7>*s91u#rJXkf-T0qbTgp`2PSaM{P# z{bCv$${62S`($K-)~R7C+~YZtT$@EfhR7`MH+6HC@OLSdiW=0tGBK@oFaFd`A~ zt#HfpTq)zT66>miob6Ao-Qn1GvQw6{6440T+KD zyVld^=lPHgQENU@KYjBNFgfyl4#muO0HHDi@S9`v!ZUlo0K`eQsBCZsuxoK4*xc%9 z_(XMXkgRgws;E`hZ_#vB8}?$zKR@@4Ci+_8u2vj)ZsDSDRfsxc;YK-jy4_UwzNid8)ZAj+p!uaTOn~7}P zojd~zDRMpZ1hb}cSRI*Toi4Y;;ZaXb?+rs>OAij8Gy_IDPv0)#!JQx+XlUFi?A0h8 z-VyaFzdbx@C2x#sG~mxB*AMvf1eSx?&o?gJye;VTW?LwW`OvAXJqU=SMhKG#DG+}y zSnCUa_bxc{2D9ctQ*2TK@b;XL72|2}W}5*TSYP6L_is-ECnyX2My=CJvDl7Vk>agy z-~XGlfiL}576xkLv)loA?9_%n8ZzU~P20H-jx!E5VSLgHu+eHA9f-sQ=$pj99Z|JR z7GfoGgcl7{roU6G&*eOOn$(7@exicEcrenuPV*iXKo^Sf|n@!Qz1=x)I zwWHo4@=|Jj7DtIC6N@*-R@Ck*f=MzH?;DEfRqg{}tdPW))^S%%2y^0F$u0qKlNTx; zDgxi}O>kBw9#-Bm9i^xF!8-QZQOO4YL`g;26k_ zC8)uHQ-igIN&rH9uy;S}q`%DUE3oBJHrY`H#pmmdQ`LZ|&bI>vH$8%6vkHx`b ztj=q2kkPO&Ks-4IS%oMEMLFV=_9_t=l?`WEzmUP)8exveH@{LHYTsnbGnT(^u9skyG#Rf=X^jWE>0oQ*~~g1s0&na z79?F|BoYD7qmy=j-rBtSop3vL%SV%qD>{E^poGoASF@AJmEHPemc3)+*j;~=O(?w! z`MiK?#r#}-6$mpTWMH(qRObM_35U>z3K)cHs_$kaK?SsBFlbNjNeFd!FHpoSYp9gi zS^Kx_ET4QBWpW?6_(=M(Jh+`YCs(w5t>CZ7-Sgaw<*TjbCTrhSIjY{mT^D2{zTlOs+F^hqk0Br3%~U=PxPidOES&;Y z73SCd+r#r#^8UDS4I7>R&vEiz9a~m8{26~xKzw;0xLkr>Bk|Lz_#O$9!!vhDdYBen4gjwWJ#|Bwi)%6Q=bP!6JQ~-n#0{}& z$^9dr-@F&kJ%9{b$vY%Q@tuDRN%XyWD&qYyR167seOaz6EP|as zI~qcW%3cgK)&#?HWGFtCN>W|VAIRz7F#3}H*NKv@cyN8*&qwgpk{*`$fq{Pu5I`rO zjW^j+YM`HkN%>naGTnCjHiv5o28(%Ce8;?n3UkAj9@!TDL^f_i`)IH5xqGK%L~KFh z)!f9XG#3+M>Q7B$PQ=D?C<*U=tvf|DQG|oh?=(G>Sjg;T({n5?a%J^xUPg(!z*M2c zD4L;^q3z19Z1U+{nRITH9PWQdij8PtZU60^o*tp7yjEzf*B++CF)#@RJfp!^S8PhJ zXg;hlYBg9@<=VvNGnESG)^QV{&_dqKQ$!bGvQ@*^Uzgu?X!d_Rqn))Y@r_Zj z*YJ?j(bd=4^&FO&g`0#GW^oDo3Ea|Js>^BKsG%>P+%Z#l(~=u}^s5SR z=gO@p;af@YYYT#YwSHxp4Qvq_>?f?%V1xa@7uZbh8Uyf?LhG9N=9OD0Swb5gWN6xX zn+>j3M0&>}jPHJ_OANmclYix(-YDD+HQsHYx=ZMc!=;CEMo@nrsF%d`LAl^()2S}m z;x3uPXDs=Fw5^NFDxO1cPmHZ|`#u1z10)`cHNA`yNsMc|<#{6j_CEh`gWd4CV!z{k zrAuCW9Jy8-BXp-|L>A!PeGqr^h$7IwDgb}XwcpcA2LxHqO-t(t_-W;0-*~PK{MwWGX%Onb@z6`|geVWKTskie z`)O_WZ|YMc9JTh{l^wMZN!(MzCR*jG`<%#Yv9Xr$)UX+M;CpJ%2m}Kw+2!MXwWCtn z?Ve?GI3)7R*=;t2+(w~pDv50y*M|ZM?~DNU!W`+(5AlD=zJ0-8aUchOj8{WmnX2_h z-YcW(*m#?JWgdh6lHUMvf%fZ+*!ZS8filTh`GgWHgd=R9AB=^_hmJIOsDsZ?sFhcQ z&I|05Y|cPy_Y~HqR4h$P1WbxUdTyHjTgx?~> z*(g8>lp@%(0R$HK15dV{-}EQn&EEau@`oQ2teAlJU*%I!11#&?EEB*3Y{TGMiK%L4 zC4HWLw{~s!sqv6!_W0pTU@)H7qkn*(_pK8iNZ38W?F`#rv3NKj8pRwcCH9 zOI~b34>tV^)uN^Htm-tz@b_eBrr%v3m%HOw49OvJ2tR0i`XL4=jN zG{`lUFq6t27+&I+vI9DEF8F-Ds>oo?BBGZ|Gl+&!R zuSGZCYdMz>F4$yea6^YnF<_WIShRmhk~<-7QC$SME3SkX_?;oR=xd*oZ+{z@Z~9JI zXga{$?Sm2x+zH+1{sYsj}&z`1{;`DwQK+qZvrD6prXb25afggB4-%3GBP&eAXZGYq-B z$0zDtb@_F;`J8i4L|i3-AexcFZ($^ za_oA__xmD{%b)A>0pRE8{rN@xv`;mbh{!x8 z7=6OgVX|29QY>CkcZG{RJHnP|6Y`#RtjpQ;-f|2ZLX~$J>1P?8+kSuWo<$QhJ;nR!_cb^4O3U}5N~v5#djdo zIX7{x6H5=^-4n-usc&db!fT?`nOtr}NhX+~yh7x$KRR+bx{Me9&Suj$)5YYfF{!|e z38-zm1~c@2=SdkeCYoqXN4u3wsC*O07giMH9NwVozHC#zHCun&9D*(p;oi{5uv8gj zI>MG4PniP^auG$!1!Qu7XKh~Mg*SR|zb@gBT4rXjrgzhb7koz3A7xg69j}4BAkKia zM5$SiL7e^@)5>{P%umPgDn#*3f0>W_BeOl;TeoT@%W{o!RbC4%DAewT2&N$nzwgiHc^F4&tsD#X4?F}+pv{5}`|Ae( z442t6BZYMv_9;MuHniV>3J^d0M^Hhj3@5}XFtqe}h6aB=#Wm-RpX;X)8F&QWEF1~u$yX3mre=PV!`>=}0GbLU`~x>A zQ4W9LAI$!3_!B*?s8C{)2beygeclXvm`Lafc8RPGc~8zA{2Cqn4JFVOY+PdXFQtv} zA48_|^VwoJpUx6Zl3siO=tpYKiS|}2sB&*H8dYcTd?Zlq!qT`C@GOpgwou>4_hWH< z*q63(3KA&(2&Ag_B~Q>n0xpYvTNVeH7kYo9egb>bud=1S%sUf%E8y6Rmb%`44tvH9 zIc{!Q6-`02Nzn-~h|_+-L0?)-;bKJJCFXLMBePC~cq@4tw3$21uh|qY5su`)IdU-x zQtH4)fa&N;XhulQpaT5vmTPr`3jB|z-~mWe(imhDs&n9K7Gg67bwIFIxGC84mCb+d zvMb5ptL(bJ7|r<`8WfjfoUF#dHF&d@3>0COn|W>20}uGju)aiwr>ZOVitYIt;IUQz zHP$%1XCGHOHb7-flgo5Ee=8*Lt@+wOHN3aGSb$@7WN0-#yk~>*XgX|Q;kJ@6RL2Iz zDAy>{1^t~%_*nZytt0;}#^XBXCdPjWmv=!`(vPOlUK;ADzsuDQF0YcKk9s-5h)p?e z{`0jt_v~1r4T3U56IvD+FQW_lK0eM9uFn$0tB@ct?2r^{ zNZ@y6aTV4P0y(AxqC=Bw-F4W1NYAAB*5z1+;(r^PG>F zOZ+z|6#F4YfB2)C2(fOXPDw!nRR1Iv6Tn;EH~R(qe1VWV?ATvT0Eqg&Od3BWfBho) z>8_o8@mF|S9P_nlaaDo+a(cUhtvn41n`Zskk{Gb8sYugINRYZ&(KB9-N|Ig0QL`eI zBx&-6En8Bpl!~q!#yo+RxblAw`^E_4nzruH19-GOWqVrkOe@}6^FpR(Y+^pA4UZS8 zIoToC!nbCgN7p{|0v=r&+nDUlN`ikF)uz)*mMPli zdEHowCtKJrseL4S$zP^frY{2fQNNsy$BTKN<9)91{sC=GF^R?>0u;a|PlpKDp6T2i zwt`e!1==JuLm7v~X;UCbLQaZeI?OFX9Q@r(DC)75e5yvmC->VDzEvZO)r5?xL)^6h zD@l~}N}xeagu?>719N|lE}!^Y9E7Q&Z3Tz+t^)5&+CXs^!|ghNnIED$;24O9M+U5l zISgrF^_TT=9Jo04DY#W}1PsI@J^>t0289Gg<7N$muRR9#V^Y)UUebTO&#p(=(o)}< zY(SlqvDFJ{m1+c<6gHRB+3bn>ds(f+v(=c5aI<{4PItCbz#V_Cc)7CeuI zCzb$(Sg?0{v&=JMP{P#^f_ewmFjK+86Cqhsw85~UkXyr!8^VDx{M8f-H_fGm!aV73jG(C|T4 z3=yHq*W&fkz>l$8?M*3Tx2P9nw|z zKcd$_D69(g!1%|@=rr$#Nj{uj!M>Mxh0Qm8xjTk0tS5gz{oCJvI{V@M`|tjCa{lh8 zZ%)76XHI|mD*Jv4*`fWTWNRzk+YVMg`KMcbyW82*)xZAkA93K@-LxI5?Ze*b_PVvOvWd)(7j(q+H&*neB>zilp7vB%v~&C|(A zQRE*c+12->{v>PUsAnTWNcrAEIrPxTljCCsvI&2QF4nC`4vAu>fev;`rRJ;K3=wq% z_p1-?(jISY)Z!@VbUHoupKkN_{KL)JVm6z8U>IWnw+K}U#g{2SyoG;!`SCWt=JN^D zI-;dU;OptHRr~j(uDkanZ1wK7)199U`=kDh=Sk@<8w@-}H;YVflVgHxo}A&Wd~9VS z57~dF#z$#O2_t;Pl2-{TioXDB?GFlm9yf`Zt^E0J!v1CP$XCdyXAj@Q5aPA3w@Bi%^84TZGJnQWdCJVRmblU zQ;rl@>M=!TCgwAy-;CL~+q3D|>DDVva9i%Ac%j&GXzI#i-;L&hc#&7sx>rcEwz3@~ zpD%UG3YQ`ID*$UK0Twye=?s~8<8B{YJQwPI5|g0~@NEVFE8$ZHmv!wRV~K)5U0i>` z6H6OK>@zsEF>f388xgU4< zzp4F{Ci}|V1$@>kDmAGGa)4;H+(q7?C`cHm2i|9na5BJa-3%|N58us4`x*|r0Ra(g zfzf7N_-k(PRlkKF(yQsyPA7M)_kw>lxXmV4Wh%;JWKZ7uUZR@rbj&X*07TmYEXI>-yn*ib>Y%3&$%}THT4j|44uGjY*^;qUvQmd)vcycRXc=>4_7Pf2XHXSYVUBeS z>w~(MPs6x0lpefrl}UWB<1)Zk1cRGf;V??|&>2;*Pv9W56A*l^B2?`_h!In_f07{1 z!o3u=u^Ij@#^}|Irx?olI~+o&?(@iUyj7aB&cJKV3HY+OHfxexQiWMdgv=jIY+C|%$QV*3iILW%B(zM;IM04Nf3T#Yw2{9!m*>m zHEoML_%9XuDXf#nuaBk?->>-yI-knQ3zBQnV^#rKG{*Jaa+F1O99N(>Civ7X`h>K3 zUlsyhbYjUoG0O|^CAoj~Ddz9aV#wF5^|^#@p>Nf!t&l)TO9PKwZ7H7XDZx6Vy{%;a zc)f;=?rs7ahTAh>No2%FH}3KJ=kfY;xBeM#AiH`cVTd|h5X8&%qH;^tweD1^qXe>h zBEZ497LECxv=WqpIhJ?S1bOeyXE{ai`m2}CX(e~X+LY*tt!saIE+*Ha zA)M%{HCwoz!tFJ1Rs0>Z?W^gpllhdGAfOI-*c0W&MXop3Vi<*Psi;Iy{ay2uY&nmQ z34k_{TI27ZDznFk1K9u-;so@4Z4UvkloQv&fsZEh;fEO_>sTxLCbie{4gsZi!fkE0 z)!o9Kt@_ndrqX}H15vELc8r)J1Oq&Qda3q#2UM&+O4{niA&y#8^rE74OVTkv+PN4k z<~l=n(KL$@KdRh}S|<1rrDA}GAvLu7ds(GJYdM1TqgFt4*iZ(OI)gtLDacPKC}y#b%P4FeEMjuQKp z`(KC~Enu62wcxIXmLu+Q)t6&khaQNIoa{QM=)O$xc`dcZdvU4zh>m%|t|}%ztxmu2 zXs^7|d?G8!zhNWcx|IAh1Z@ZRMuVz%ptBUYH)L4ol_ zG;?BXdO4|`?FyXgYzJA@*(Q0#TKt~O>TJijWoX9iVkndRs%zch_cHJ`HzhlvYz2qM zP2`s^Z+NEtI-kJq@US_kw_opu#ZThl_37lN>@I(st$q^D_#pvM{E9F)m>upXLsn*w z%6JXGU%bi1xHA+xjMCnL`e^nC@m(xjQmTl1zD;^73@`GwwXim#v6&pnu>?z>_m}Dc z-U%W0Rj|bvE~o4-^Xd4(U}!38ob@2-5R{8Eh^CHul&S(9vd(dUAQGNtnUk6EWpi49 z)EdRzzJMQpT>ZDjbt*Qg6?c-l16{5Jbjmr&H`DNoQ5VxjAg4vXFGrlao)^HMe85t*Si*f1o(irh;5Pq8tT>p_hvQEY($0& z?(!FCfOLA*Py3AlE{E{=5wr@AhI%mah*k|+$p90$m|u5OSoQN7#3y$ayA)1LLcYvs zRc(o$)w;55>~pDRtl;SyYWhsd#(HqHt+V}{>INZ(+i@L*s}Y3MRyl|A3OeVs_+6Dw z22E;zmL&gl4Z|+7@h^?8+y*+L`r)_O%4(K2)PqAP8DXus@po#1`4aWUp@5QNC?J#p zhy#OrJ6#M&aB9jd2V=3p_Q`hDD(K!3XuiYEvyUnah;J089tAQMbPbQ*{bM@gsadmN z#N!}Sb|_94Y+1pORlL2m)!m9>AL4gC>{H8sn+n;ytimM5{mx~x3hn%oM`rSqD^sSf zkP^Y0#~U7}$rCO-M&pw>1LM#fiLe>;|2I+pF*i|Hq(^QGbiLRycrgy8s$O~tSfj7D zYdZ$l=70`a76Xw6K&Sq8K9$IQ`W@ehJKQktXn%62{Rl?c!$2?+%&Kwc5#iMqyfL+Z zOUT2(*C8}ipLscw~hm*R}Q&p@ZiCm`CMpZ}_$%C%NtE76pU7NWhx@h$ zLjwM2H?`|REV7j9^S;Q_-(<7wfk%6Bo%8uC@laZ2EwLp>T#YNtjCcQ_6Jv5p8=N8k z)>GO)=R_P~-7UrXe3sw-(Xj4+m16zB7yYZ*;*Wv&@1OU8oTNSXm(xlo2g2)tr%!i& zrxb^p?mjBj;gf5|7gMIjm(E_#V?dgA6?b5fStmI(gZ4U628E2K9)r4%%K>?OjL)AR z%SXQR`X-;DqEr?&8U`K+KJ5W+o$WTsS$=z0BTct_v9M?a8U{on8rofdb$7xow)SLK z-Cd%qy=YfWM?VbZ71Sf*o$6^w?>E&DuX;$$S@rI-Dint}UCib;rmP!KwjRGNq9Y~} zA!X}zd=2Pz>ndBX7jDt(mg zwYw>1HmdZ=fM7#3Pr!82KxSDn8sf)$*0Qop0^+lRi<;7Fnbs8q>3E-dvaGP2Kt+R9 zr^7FtEtb+e_jWp4orB*&)C;tzvA4b5-nEt@QdH5bZFF|KTWwi$SJv!?w5JCP3XACS zgRK;eg|+$ssl8r*GpvDxS_Kr)4q?~Vz!rk^Ctv^I1~PV{sJ+t$2O%aE9+^=b1bDqW1o0%T#H+_ z|FTz6R%XeASNKcPrIs_6Xst!o^HxwAE3=SWeR-?HoOG>!1ukr3Pa_pO!|)(`bPmDXp>0 z=}sqq3th0Ig|SX}p;!nj$_}-Tnfi*-<6%>esQt;W9MQh0RvG0(RIH(W3$d`e+mvCM zS#qtXm;Ne$>294x(zD@BHqPv&(6elo_ec3Bo@NW405Dly*!(?UY(ObBVqf<_M152g zQ0NXVXkt1MMZoWH038m>&Mr_FV`;K6LKP4&#)TUqCN`}r1yHxzm2|l);aDITXEa-^ zE=?VajiSqeW)DC9{8@%{!8SrQkB)S`fDr34I|#UcLVMHepacw2V<7(47fO_#bi_v- zU(`4|N$u|EmO0=VbqsftpUer_sKUv%$Zxak>hRrh1N>Jm9-k1m;b*hibhe+o16xrS zAAYx(52xeoJ^z!nvSv0K0-h>-&z#kU8~A_K&qo^#-hs9jc*2j9B@^tg&W{;!kjiBq zN}NJ}7tctZH)WUjCU}4d?`YfCmY8kJ?rWLf&!)G1xD#DAJpAFfVNRF)pdOylL!yC% zVUwWsR%3>$3&w0{R$$Ckhc2AIW%KW5>a9s2TftLJ$Nl;6hCll*KMdiG0KqC|qvr9P zJ6sNUH>_gW1&PG@RLi=76heMHZzb=J*Td<5Y%v^WMWM3NLFANRwX#q+O0{&5G+)<4 z5mdJvxfo{5fgFDICA{nME3-YVUQDxJA17aZ$#DGYOA9wq5u$`bL3GVSvi{ZkR`Ti{ zn26@2Fpu{zqFY=8Zd5iI`L&kSG-g^OegKVVYHFm~TR@$jII)`%CL()!@7a@}eNB^p zdaps2=!WEQVF}-=q8VPpvV=AuxAVS|qLRpn<*;TsN(hM zQpw(flGQLF52#Y#Z?j+D0rY=x=fFP_hyB4{Vku zzoxxcGj>8N922+AP%|i``Apxr=cs9a0GwV|^=BS`>*&3bw#El5+Bzsnsh4796rtMq zq1pcw+J7#UTZ7jI&`PYZ!;JP-jUmJk3AQR*BsIno_>Te}GalLzY_0J1Pz_Ovh*0oq z`7rApbbsUz7^xbrwW)4MTisaGST|}7&3IULO|~QiAO>dfkk$VMP)h*<6ay3p00008 l0QZJ)lY~w<4)=y|SMF-vHI_{P01?}h%1$c=j!pmo005m86wUwu diff --git a/Source/DafnyStandardLibraries/examples/Arithmetic/ArithmeticExamples.dfy b/Source/DafnyStandardLibraries/examples/Arithmetic/ArithmeticExamples.dfy index 974d53f8a91..5c9ecbbd98b 100644 --- a/Source/DafnyStandardLibraries/examples/Arithmetic/ArithmeticExamples.dfy +++ b/Source/DafnyStandardLibraries/examples/Arithmetic/ArithmeticExamples.dfy @@ -1,7 +1,7 @@ module ArithmeticExamples { - import opened DafnyStdLibs.Arithmetic.Logarithm - import opened DafnyStdLibs.Arithmetic.Power - import opened DafnyStdLibs.Arithmetic.Mul + import opened Std.Arithmetic.Logarithm + import opened Std.Arithmetic.Power + import opened Std.Arithmetic.Mul /* log_b(m * n) = log_b(m) + log_b(n) if m and n are also powers of b */ lemma LogProductRule(b: nat, x: nat, y: nat) @@ -19,7 +19,7 @@ module ArithmeticExamples { LemmaLogPow(b, y); } - module DecimalLittleEndian refines DafnyStdLibs.Arithmetic.LittleEndianNat { + module DecimalLittleEndian refines Std.Arithmetic.LittleEndianNat { function BASE(): nat { 10 } diff --git a/Source/DafnyStandardLibraries/examples/Arithmetic/ArithmeticTests.dfy b/Source/DafnyStandardLibraries/examples/Arithmetic/ArithmeticTests.dfy index 3265bbde518..343b85a4c17 100644 --- a/Source/DafnyStandardLibraries/examples/Arithmetic/ArithmeticTests.dfy +++ b/Source/DafnyStandardLibraries/examples/Arithmetic/ArithmeticTests.dfy @@ -1,11 +1,11 @@ module ArithmeticTests { - import opened DafnyStdLibs.Arithmetic.Logarithm - import opened DafnyStdLibs.Arithmetic.Power - import opened DafnyStdLibs.Arithmetic.Mul - import opened DafnyStdLibs.Arithmetic.Power2 - import opened DafnyStdLibs.Arithmetic.MulInternals - import opened DafnyStdLibs.Arithmetic.ModInternals - import opened DafnyStdLibs.Arithmetic.DivInternals + import opened Std.Arithmetic.Logarithm + import opened Std.Arithmetic.Power + import opened Std.Arithmetic.Mul + import opened Std.Arithmetic.Power2 + import opened Std.Arithmetic.MulInternals + import opened Std.Arithmetic.ModInternals + import opened Std.Arithmetic.DivInternals method {:test} TestMul() { for i := -10 to 10 { diff --git a/Source/DafnyStandardLibraries/examples/Base64Examples.dfy b/Source/DafnyStandardLibraries/examples/Base64Examples.dfy index 48da3ab5e00..dc1e2fe35d8 100644 --- a/Source/DafnyStandardLibraries/examples/Base64Examples.dfy +++ b/Source/DafnyStandardLibraries/examples/Base64Examples.dfy @@ -1,7 +1,7 @@ module Base64Examples { - import opened DafnyStdLibs.Base64 - import opened DafnyStdLibs.BoundedInts - import opened DafnyStdLibs.Wrappers + import opened Std.Base64 + import opened Std.BoundedInts + import opened Std.Wrappers method CheckEncodeDecode(uints: seq, bytes: seq) { expect Decode(Encode(uints)) == Success(uints); diff --git a/Source/DafnyStandardLibraries/examples/BoundedIntExamples.dfy b/Source/DafnyStandardLibraries/examples/BoundedIntExamples.dfy index 33dcf7aa3a2..f4537d5457a 100644 --- a/Source/DafnyStandardLibraries/examples/BoundedIntExamples.dfy +++ b/Source/DafnyStandardLibraries/examples/BoundedIntExamples.dfy @@ -1,4 +1,4 @@ -import opened DafnyStdLibs.BoundedInts +import opened Std.BoundedInts lemma BoundedIntUser(x: uint32, z: nat16) ensures TWO_TO_THE_15 * 2 == TWO_TO_THE_16 @@ -15,7 +15,7 @@ method {:test} UseExterns() { } module {:extern} {:dummyImportMember "NonDefault", true} Externs { - import opened DafnyStdLibs.BoundedInts + import opened Std.BoundedInts class {:extern} NonDefault { static method {:extern} SquareNativeInt(i: int32) returns (r: int32) } diff --git a/Source/DafnyStandardLibraries/examples/CollectionsExamples.dfy b/Source/DafnyStandardLibraries/examples/CollectionsExamples.dfy index e50d60adbd4..b0e46272b1d 100644 --- a/Source/DafnyStandardLibraries/examples/CollectionsExamples.dfy +++ b/Source/DafnyStandardLibraries/examples/CollectionsExamples.dfy @@ -17,8 +17,8 @@ module CollectionsExamples { module SeqExamples { - import opened DafnyStdLibs.Wrappers - import opened DafnyStdLibs.Collections.Seqs + import opened Std.Wrappers + import opened Std.Collections.Seq import opened Helpers // A sequence that's long enough to be non-trivial @@ -116,8 +116,8 @@ module CollectionsExamples { module SetExamples { - import opened DafnyStdLibs.Wrappers - import opened DafnyStdLibs.Collections.Sets + import opened Std.Wrappers + import opened Std.Collections.Set import opened Helpers method {:test} TestSetRange() { @@ -137,8 +137,8 @@ module CollectionsExamples { module MapsExamples { - import opened DafnyStdLibs.Wrappers - import opened DafnyStdLibs.Collections.Maps + import opened Std.Wrappers + import opened Std.Collections.Map import opened Helpers const m := map[1 := 10, 2 := 20, 3 := 30] @@ -160,8 +160,8 @@ module CollectionsExamples { module ImapsExamples { - import opened DafnyStdLibs.Wrappers - import opened DafnyStdLibs.Collections.Imaps + import opened Std.Wrappers + import opened Std.Collections.Imap import opened Helpers const m := imap[1 := 10, 2 := 20, 3 := 30] @@ -175,9 +175,9 @@ module CollectionsExamples { module ArraysExamples { - import opened DafnyStdLibs.Wrappers - import opened DafnyStdLibs.Relations - import opened DafnyStdLibs.Collections.Arrays + import opened Std.Wrappers + import opened Std.Relations + import opened Std.Collections.Array import opened Helpers method {:test} TestBinarySearch() { diff --git a/Source/DafnyStandardLibraries/examples/DynamicArrayExamples.dfy b/Source/DafnyStandardLibraries/examples/DynamicArrayExamples.dfy index deb97ea1266..8c1807626d0 100644 --- a/Source/DafnyStandardLibraries/examples/DynamicArrayExamples.dfy +++ b/Source/DafnyStandardLibraries/examples/DynamicArrayExamples.dfy @@ -1,6 +1,6 @@ module DynamicArrayExamples { - import opened DafnyStdLibs.DynamicArray - import opened DafnyStdLibs.BoundedInts + import opened Std.DynamicArray + import opened Std.BoundedInts method {:test} Ensure() { var arr := new DynamicArray(); diff --git a/Source/DafnyStandardLibraries/examples/FileIO/ReadBytesFromFile.dfy b/Source/DafnyStandardLibraries/examples/FileIO/ReadBytesFromFile.dfy index 702ce5cfd90..5e483afcb88 100644 --- a/Source/DafnyStandardLibraries/examples/FileIO/ReadBytesFromFile.dfy +++ b/Source/DafnyStandardLibraries/examples/FileIO/ReadBytesFromFile.dfy @@ -4,7 +4,7 @@ *******************************************************************************/ module ReadBytesFromFile { - import DafnyStdLibs.FileIO + import Std.FileIO method {:test} Test() { // TODO: extern function for the expected error prefix diff --git a/Source/DafnyStandardLibraries/examples/FileIO/WriteBytesToFile.dfy b/Source/DafnyStandardLibraries/examples/FileIO/WriteBytesToFile.dfy index 2013c447dbb..eac8ed2b1d7 100644 --- a/Source/DafnyStandardLibraries/examples/FileIO/WriteBytesToFile.dfy +++ b/Source/DafnyStandardLibraries/examples/FileIO/WriteBytesToFile.dfy @@ -4,7 +4,7 @@ *******************************************************************************/ module WriteBytesToFile { - import DafnyStdLibs.FileIO + import Std.FileIO method {:test} Test() { // TODO: extern function for the expected error prefix diff --git a/Source/DafnyStandardLibraries/examples/FunctionsExamples.dfy b/Source/DafnyStandardLibraries/examples/FunctionsExamples.dfy index bf617a4e51b..29692a15942 100644 --- a/Source/DafnyStandardLibraries/examples/FunctionsExamples.dfy +++ b/Source/DafnyStandardLibraries/examples/FunctionsExamples.dfy @@ -1,6 +1,6 @@ module FunctionExamples { - import opened DafnyStdLibs.Functions + import opened Std.Functions const square := (x: int) => x * x lemma TestInjective() diff --git a/Source/DafnyStandardLibraries/examples/Helpers.dfy b/Source/DafnyStandardLibraries/examples/Helpers.dfy index 081cdb5e954..b8521b9fef0 100644 --- a/Source/DafnyStandardLibraries/examples/Helpers.dfy +++ b/Source/DafnyStandardLibraries/examples/Helpers.dfy @@ -4,7 +4,7 @@ *******************************************************************************/ module Helpers { - import opened DafnyStdLibs.Wrappers + import opened Std.Wrappers // TODO: consider tweaking /testContracts to support this use case better. method AssertAndExpect(p: bool, maybeMsg: Option := None) requires p { match maybeMsg { diff --git a/Source/DafnyStandardLibraries/examples/RelationExamples.dfy b/Source/DafnyStandardLibraries/examples/RelationExamples.dfy index 6b35cb45444..4f485f8c547 100644 --- a/Source/DafnyStandardLibraries/examples/RelationExamples.dfy +++ b/Source/DafnyStandardLibraries/examples/RelationExamples.dfy @@ -1,6 +1,6 @@ module RelationExamples { - import opened DafnyStdLibs.Relations + import opened Std.Relations const partialOrdering := (a: int, b: int) => !(a == 9 && b == 10) && a <= b lemma TestRelationProperties() diff --git a/Source/DafnyStandardLibraries/examples/StringsExamples.dfy b/Source/DafnyStandardLibraries/examples/StringsExamples.dfy index 15adb0681ea..d2924bd7815 100644 --- a/Source/DafnyStandardLibraries/examples/StringsExamples.dfy +++ b/Source/DafnyStandardLibraries/examples/StringsExamples.dfy @@ -1,6 +1,6 @@ module StringsExamples { - import opened DafnyStdLibs.Strings - import opened DafnyStdLibs.Wrappers + import opened Std.Strings + import opened Std.Wrappers method {:test} TestOfInt() { expect OfInt(0) == "0"; diff --git a/Source/DafnyStandardLibraries/examples/UnicodeExamples.dfy b/Source/DafnyStandardLibraries/examples/UnicodeExamples.dfy index fd841ae74c9..c95ff858492 100644 --- a/Source/DafnyStandardLibraries/examples/UnicodeExamples.dfy +++ b/Source/DafnyStandardLibraries/examples/UnicodeExamples.dfy @@ -6,7 +6,7 @@ module UnicodeExamples { module BaseExamples { - import opened DafnyStdLibs.Unicode.Base + import opened Std.Unicode.Base import opened Helpers const TEST_ASSIGNED_PLANE_CODE_POINTS: set := { @@ -32,9 +32,9 @@ module UnicodeExamples { } module Utf8EncodingFormExamples { - import opened DafnyStdLibs.Unicode.Base - import opened DafnyStdLibs.Unicode.Utf8EncodingForm - import opened DafnyStdLibs.Wrappers + import opened Std.Unicode.Base + import opened Std.Unicode.Utf8EncodingForm + import opened Std.Wrappers import opened Helpers method {:test} TestEmptySequenceIsWellFormed() { @@ -89,9 +89,9 @@ module UnicodeExamples { } module Utf16EncodingFormExamples { - import opened DafnyStdLibs.Unicode.Base - import opened DafnyStdLibs.Unicode.Utf16EncodingForm - import opened DafnyStdLibs.Wrappers + import opened Std.Unicode.Base + import opened Std.Unicode.Utf16EncodingForm + import opened Std.Wrappers import opened Helpers method {:test} TestEmptySequenceIsWellFormed() { @@ -142,12 +142,12 @@ module UnicodeExamples { } module UnicodeStringsWithUnicodeCharExamples { - import opened DafnyStdLibs.BoundedInts - import opened DafnyStdLibs.Unicode.Base - import opened DafnyStdLibs.Wrappers + import opened Std.BoundedInts + import opened Std.Unicode.Base + import opened Std.Wrappers import opened Helpers - import UnicodeStrings = DafnyStdLibs.Unicode.UnicodeStringsWithUnicodeChar + import UnicodeStrings = Std.Unicode.UnicodeStringsWithUnicodeChar const currenciesStr := "\U{24}\U{A3}\U{20AC}\U{1F4B0}" const currenciesUtf8: seq := [0x24] + [0xC2, 0xA3] + [0xE2, 0x82, 0xAC] + [0xF0, 0x9F, 0x92, 0xB0] @@ -178,10 +178,10 @@ module UnicodeExamples { } module Utf8EncodingSchemeExamples { - import opened DafnyStdLibs.Unicode.Base - import opened DafnyStdLibs.Unicode.Utf8EncodingForm - import EncodingScheme = DafnyStdLibs.Unicode.Utf8EncodingScheme - import opened DafnyStdLibs.Wrappers + import opened Std.Unicode.Base + import opened Std.Unicode.Utf8EncodingForm + import EncodingScheme = Std.Unicode.Utf8EncodingScheme + import opened Std.Wrappers import opened Helpers const currenciesUtf8: CodeUnitSeq := [0x24] + [0xC2, 0xA3] + [0xE2, 0x82, 0xAC] + [0xF0, 0x9F, 0x92, 0xB0] diff --git a/Source/DafnyStandardLibraries/examples/WrappersExamples.dfy b/Source/DafnyStandardLibraries/examples/WrappersExamples.dfy index 13d3ee9358f..2daa199ae08 100644 --- a/Source/DafnyStandardLibraries/examples/WrappersExamples.dfy +++ b/Source/DafnyStandardLibraries/examples/WrappersExamples.dfy @@ -1,4 +1,4 @@ -import opened DafnyStdLibs.Wrappers +import opened Std.Wrappers // ------ Demo for Option ---------------------------- // We use Option when we don't need to pass around a reason for the failure, diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/DivMod.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/DivMod.dfy index 09604b28bd7..a49bfed4999 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/DivMod.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/DivMod.dfy @@ -10,7 +10,7 @@ former takes arguments and may be more stable and less reliant on Z3 heuristics. The latter includes automation and its use requires less effort*/ -module DafnyStdLibs.Arithmetic.DivMod { +module Std.Arithmetic.DivMod { import opened DivInternals import DivINL = DivInternalsNonlinear diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/DivInternals.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/DivInternals.dfy index bd1620fa3fb..25f8e976da6 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/DivInternals.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/DivInternals.dfy @@ -16,7 +16,7 @@ This may produce "surprising" results for negative values. For example, -3 div 5 is -1 and -3 mod 5 is 2. Note this is consistent: -3 * -1 + 2 == 5 */ -module DafnyStdLibs.Arithmetic.DivInternals { +module Std.Arithmetic.DivInternals { import opened GeneralInternals import opened ModInternals diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/GeneralInternals.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/GeneralInternals.dfy index ef39b22606d..7908669ad8f 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/GeneralInternals.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/GeneralInternals.dfy @@ -6,7 +6,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -module DafnyStdLibs.Arithmetic.GeneralInternals { +module Std.Arithmetic.GeneralInternals { /* this predicate is primarily used as a trigger */ ghost predicate IsLe(x: int, y: int) diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/ModInternals.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/ModInternals.dfy index 2acc2dd5082..d3ef0518d7d 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/ModInternals.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/ModInternals.dfy @@ -16,7 +16,7 @@ This may produce "surprising" results for negative values. For example, -3 div 5 is -1 and -3 mod 5 is 2. Note this is consistent: -3 * -1 + 2 == 5 */ -module DafnyStdLibs.Arithmetic.ModInternals { +module Std.Arithmetic.ModInternals { import opened GeneralInternals import opened Mul diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/MulInternals.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/MulInternals.dfy index 1fca7145826..81c964d220e 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/MulInternals.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/MulInternals.dfy @@ -8,7 +8,7 @@ /* lemmas and functions in this file are used in the proofs in Mul.dfy */ -module DafnyStdLibs.Arithmetic.MulInternals { +module Std.Arithmetic.MulInternals { import opened GeneralInternals import opened MulInternalsNonlinear diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/LittleEndianNat.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/LittleEndianNat.dfy index b416dea07f2..dd82b7afa0c 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/LittleEndianNat.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/LittleEndianNat.dfy @@ -11,12 +11,12 @@ Little endian interpretation of a sequence of numbers with a given base. The first element of a sequence is the least significant position; the last element is the most significant position. */ -abstract module DafnyStdLibs.Arithmetic.LittleEndianNat { +abstract module Std.Arithmetic.LittleEndianNat { import opened DivMod import opened Mul import opened Power - import opened Collections.Seqs + import opened Collections.Seq import opened Logarithm function BASE(): nat diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Logarithm.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Logarithm.dfy index 06a83414a76..4670e0dd1a5 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Logarithm.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Logarithm.dfy @@ -1,4 +1,4 @@ -module DafnyStdLibs.Arithmetic.Logarithm { +module Std.Arithmetic.Logarithm { import opened Mul import opened DivMod import opened Power diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Mul.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Mul.dfy index 919adb675f2..ce0c1e604e4 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Mul.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Mul.dfy @@ -10,7 +10,7 @@ former takes arguments and may be more stable and less reliant on Z3 heuristics. The latter includes automation and its use requires less effort */ -module DafnyStdLibs.Arithmetic.Mul { +module Std.Arithmetic.Mul { import MulINL = MulInternalsNonlinear import opened MulInternals diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Power.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Power.dfy index 0767a84377c..8b22a3e4946 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Power.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Power.dfy @@ -10,7 +10,7 @@ former takes arguments and may be more stable and less reliant on Z3 heuristics. The latter includes automation and its use requires less effort */ -module DafnyStdLibs.Arithmetic.Power { +module Std.Arithmetic.Power { import opened DivMod import opened GeneralInternals import opened Mul diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Power2.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Power2.dfy index b899463bcd8..289c439505e 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Power2.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Power2.dfy @@ -10,7 +10,7 @@ former takes arguments and may be more stable and less reliant on Z3 heuristics. The latter includes automation and its use requires less effort */ -module DafnyStdLibs.Arithmetic.Power2 { +module Std.Arithmetic.Power2 { import opened GeneralInternals import opened MulInternals import opened Power diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Strings.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Strings.dfy index d092f410f04..15d3ac81e4f 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Strings.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Strings.dfy @@ -1,7 +1,7 @@ /** The Strings module enables converting between numbers such as nat and int, and String */ -module DafnyStdLibs.Strings { +module Std.Strings { import opened Wrappers import opened Arithmetic.Power import opened Arithmetic.Logarithm diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/dfyconfig.toml b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/dfyconfig.toml index b2e6762abf7..d636bb48b5e 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/dfyconfig.toml +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/dfyconfig.toml @@ -8,7 +8,7 @@ library = [ "../EnableNonLinearArithmetic/Arithmetic/Internals/DivInternalsNonlinear.dfy", "../EnableNonLinearArithmetic/Arithmetic/Internals/ModInternalsNonlinear.dfy", "../EnableNonLinearArithmetic/Arithmetic/Internals/MulInternalsNonlinear.dfy", - "../EnableNonLinearArithmetic/Collections/Seqs.dfy", + "../EnableNonLinearArithmetic/Collections/Seq.dfy", "../EnableNonLinearArithmetic/Wrappers.dfy", "../EnableNonLinearArithmetic/Relations.dfy", "../EnableNonLinearArithmetic/Math.dfy", diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Arithmetic/Internals/DivInternalsNonlinear.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Arithmetic/Internals/DivInternalsNonlinear.dfy index b4957644215..ef73d917f08 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Arithmetic/Internals/DivInternalsNonlinear.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Arithmetic/Internals/DivInternalsNonlinear.dfy @@ -6,7 +6,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -module DafnyStdLibs.Arithmetic.DivInternalsNonlinear { +module Std.Arithmetic.DivInternalsNonlinear { /* WARNING: Think three times before adding to this file, as nonlinear verification is highly unstable! */ diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Arithmetic/Internals/ModInternalsNonlinear.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Arithmetic/Internals/ModInternalsNonlinear.dfy index 671fc4ae3ec..43a3f9fceb4 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Arithmetic/Internals/ModInternalsNonlinear.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Arithmetic/Internals/ModInternalsNonlinear.dfy @@ -6,7 +6,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -module DafnyStdLibs.Arithmetic.ModInternalsNonlinear { +module Std.Arithmetic.ModInternalsNonlinear { /* WARNING: Think three times before adding to this file, as nonlinear verification is highly unstable! */ diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Arithmetic/Internals/MulInternalsNonlinear.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Arithmetic/Internals/MulInternalsNonlinear.dfy index b47945e50b3..c990eb98c01 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Arithmetic/Internals/MulInternalsNonlinear.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Arithmetic/Internals/MulInternalsNonlinear.dfy @@ -6,7 +6,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -module DafnyStdLibs.Arithmetic.MulInternalsNonlinear { +module Std.Arithmetic.MulInternalsNonlinear { /* WARNING: Think three times before adding to this file, as nonlinear verification is highly unstable! */ diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Base64.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Base64.dfy index 7733a8bce58..cefb455de69 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Base64.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Base64.dfy @@ -4,7 +4,7 @@ *******************************************************************************/ /** An encoder and decoder for the Base64 encoding scheme. */ -module DafnyStdLibs.Base64 { +module Std.Base64 { import opened Wrappers import opened BoundedInts diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/BoundedInts.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/BoundedInts.dfy index 6eda9f9d23a..3e1f7c6f870 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/BoundedInts.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/BoundedInts.dfy @@ -1,7 +1,7 @@ /** Defines symbolic names for various powers of 2 and newtypes for various common restricted-range int types. */ -module DafnyStdLibs.BoundedInts { +module Std.BoundedInts { const TWO_TO_THE_0: int := 1 const TWO_TO_THE_1: int := 2 diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Arrays.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Array.dfy similarity index 94% rename from Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Arrays.dfy rename to Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Array.dfy index 486dd37461d..8175eb78dde 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Arrays.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Array.dfy @@ -6,11 +6,11 @@ /** This module defines useful properties and functions relating to the built-in `array` type. */ -module DafnyStdLibs.Collections.Arrays { +module Std.Collections.Array { import opened Wrappers import opened Relations - import opened Seqs + import opened Seq method BinarySearch(a: array, key: T, less: (T, T) -> bool) returns (r: Option) requires SortedBy((x, y) => less(x, y) || x == y, a[..]) diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Collections.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Collections.dfy index 07230ef9037..94aa29bcc72 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Collections.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Collections.dfy @@ -7,7 +7,7 @@ This module contains submodules each defining useful properties and functions relating to the built-in collection types. */ -module DafnyStdLibs.Collections { +module Std.Collections { // This module currently contains no definitions, // but is defined so that the module comment appears in generated documentation. } diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Imaps.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Imap.dfy similarity index 98% rename from Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Imaps.dfy rename to Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Imap.dfy index 069465c1962..3627b45521e 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Imaps.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Imap.dfy @@ -10,7 +10,7 @@ /** This module defines useful properties and functions relating to the built-in `imap` type. */ -module DafnyStdLibs.Collections.Imaps { +module Std.Collections.Imap { import opened Wrappers diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Isets.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Iset.dfy similarity index 97% rename from Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Isets.dfy rename to Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Iset.dfy index 108a1a8e03a..ddb29b823fe 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Isets.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Iset.dfy @@ -14,7 +14,7 @@ /** This module defines useful properties and functions relating to the built-in `iset` type. */ -module DafnyStdLibs.Collections.Isets { +module Std.Collections.Iset { import opened Functions import opened Relations diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Maps.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Map.dfy similarity index 99% rename from Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Maps.dfy rename to Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Map.dfy index 311b826b736..275b4c3f28f 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Maps.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Map.dfy @@ -10,7 +10,7 @@ /** This module defines useful properties and functions relating to the built-in `map` type. */ -module DafnyStdLibs.Collections.Maps { +module Std.Collections.Map { import opened Wrappers diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Seqs.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Seq.dfy similarity index 99% rename from Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Seqs.dfy rename to Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Seq.dfy index f3b4b854a10..e5c369d8f4c 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Seqs.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Seq.dfy @@ -14,7 +14,7 @@ /** This module defines useful properties and functions relating to the built-in `seq` type. */ -module DafnyStdLibs.Collections.Seqs { +module Std.Collections.Seq { import opened Wrappers import opened Relations diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Sets.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Sets.dfy index e441a551ebe..7822d127909 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Sets.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Collections/Sets.dfy @@ -14,7 +14,7 @@ /** This module defines useful properties and functions relating to the built-in `set` type. */ -module DafnyStdLibs.Collections.Sets { +module Std.Collections.Set { import opened Functions import opened Relations diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/DynamicArray.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/DynamicArray.dfy index 9f48da70001..cfbf4983dcc 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/DynamicArray.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/DynamicArray.dfy @@ -1,4 +1,4 @@ -module DafnyStdLibs.DynamicArray { +module Std.DynamicArray { import opened BoundedInts import opened Wrappers diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Functions.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Functions.dfy index 700fa3f1957..ca81854d327 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Functions.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Functions.dfy @@ -7,7 +7,7 @@ A collection of predicates that establish whether commonly known properties on f such as injectivity and commutativity, hold. These properties can only be applied to functions on value types. */ -module DafnyStdLibs.Functions { +module Std.Functions { ghost predicate Injective(f: X --> Y) reads f.reads diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Math.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Math.dfy index f9f4d7e98e9..e328be4dfdb 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Math.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Math.dfy @@ -4,7 +4,7 @@ *******************************************************************************/ /** Defines various integer-math functions */ -module DafnyStdLibs.Math { +module Std.Math { /** Minimum of two integers */ function Min(a: int, b: int): int diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Relations.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Relations.dfy index 51a7b5ce9e1..5cda42cc020 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Relations.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Relations.dfy @@ -11,7 +11,7 @@ as opposed to relations that operate on sets in general. Also contains predicates that establish how a value relates to a set, such as whether it is the least or minimal element. */ -module DafnyStdLibs.Relations { +module Std.Relations { ghost predicate Reflexive(relation: (T, T) -> bool) { forall x :: relation(x, x) diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Unicode.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Unicode.dfy index cae119b91f1..1c3acb2a1b6 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Unicode.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Unicode.dfy @@ -10,7 +10,7 @@ Unicode encoding forms and encoding schemes (including UTF-8 and UTF-16), and helpful properties and functions for manipulation and conversion of Unicode strings. */ -module DafnyStdLibs.Unicode { +module Std.Unicode { // This top-level module contains no definitions. // It exists to enable import between child modules, // and so that its doc comment appears in generated documentation. diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeBase.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeBase.dfy index f3bb9fd02d6..b333d921f14 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeBase.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeBase.dfy @@ -6,7 +6,7 @@ /** * This module implements basic functionality of Unicode 15.1.0. */ -module DafnyStdLibs.Unicode.Base { +module Std.Unicode.Base { /** * Any value in the Unicode codespace (a range of integers from 0 to 10FFFF_16). (Section 3.4 D9-D10) */ diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeEncodingForm.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeEncodingForm.dfy index 20399c4d281..6868568a5ad 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeEncodingForm.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeEncodingForm.dfy @@ -17,11 +17,11 @@ * - The function `DecodeMinimalWellFormedCodeUnitSubsequence`, which defines the mapping from minimal well-formed * code unit subsequences to scalar values. */ -abstract module DafnyStdLibs.Unicode.UnicodeEncodingForm { +abstract module Std.Unicode.UnicodeEncodingForm { import opened Wrappers import Functions - import Collections.Seqs + import Collections.Seq import opened Base type CodeUnitSeq = seq @@ -130,7 +130,7 @@ abstract module DafnyStdLibs.Unicode.UnicodeEncodingForm { * or None if no such partition exists. */ function PartitionCodeUnitSequenceChecked(s: CodeUnitSeq): (maybeParts: Option>) - ensures maybeParts.Some? ==> Seqs.Flatten(maybeParts.Extract()) == s + ensures maybeParts.Some? ==> Seq.Flatten(maybeParts.Extract()) == s decreases |s| { if s == [] then Some([]) @@ -171,7 +171,7 @@ abstract module DafnyStdLibs.Unicode.UnicodeEncodingForm { * subsequences. */ function PartitionCodeUnitSequence(s: WellFormedCodeUnitSeq): (parts: seq) - ensures Seqs.Flatten(parts) == s + ensures Seq.Flatten(parts) == s { PartitionCodeUnitSequenceChecked(s).Extract() } @@ -230,16 +230,16 @@ abstract module DafnyStdLibs.Unicode.UnicodeEncodingForm { * The concatenation of minimal well-formed code unit subsequences is itself a well-formed code unit sequence. */ lemma LemmaFlattenMinimalWellFormedCodeUnitSubsequences(ms: seq) - ensures IsWellFormedCodeUnitSequence(Seqs.Flatten(ms)) + ensures IsWellFormedCodeUnitSequence(Seq.Flatten(ms)) { if |ms| == 0 { - // assert IsWellFormedCodeUnitSequence(Seqs.Flatten(ms)); + // assert IsWellFormedCodeUnitSequence(Seq.Flatten(ms)); } else { var head := ms[0]; var tail := ms[1..]; LemmaFlattenMinimalWellFormedCodeUnitSubsequences(tail); - var flatTail := Seqs.Flatten(tail); + var flatTail := Seq.Flatten(tail); LemmaPrependMinimalWellFormedCodeUnitSubsequence(head, flatTail); } } @@ -253,7 +253,7 @@ abstract module DafnyStdLibs.Unicode.UnicodeEncodingForm { var partsS := PartitionCodeUnitSequence(s); var partsT := PartitionCodeUnitSequence(t); var partsST := partsS + partsT; - Seqs.LemmaFlattenConcat(partsS, partsT); + Seq.LemmaFlattenConcat(partsS, partsT); LemmaFlattenMinimalWellFormedCodeUnitSubsequences(partsST); } @@ -263,20 +263,20 @@ abstract module DafnyStdLibs.Unicode.UnicodeEncodingForm { */ function EncodeScalarSequence(vs: seq): (s: WellFormedCodeUnitSeq) { - var ms := Seqs.Map(EncodeScalarValue, vs); + var ms := Seq.Map(EncodeScalarValue, vs); LemmaFlattenMinimalWellFormedCodeUnitSubsequences(ms); - Seqs.Flatten(ms) + Seq.Flatten(ms) } by method { // Optimize to to avoid allocating the intermediate unflattened sequence. - // We can't quite use Seqs.FlatMap easily because we need to prove the result + // We can't quite use Seq.FlatMap easily because we need to prove the result // is not just a seq but a WellFormedCodeUnitSeqs. // TODO: We can be even more efficient by using a JSON.Utils.Vectors.Vector instead. s := []; ghost var unflattened: seq := []; for i := |vs| downto 0 - invariant unflattened == Seqs.Map(EncodeScalarValue, vs[i..]) - invariant s == Seqs.Flatten(unflattened) + invariant unflattened == Seq.Map(EncodeScalarValue, vs[i..]) + invariant s == Seq.Flatten(unflattened) { var next: MinimalWellFormedCodeUnitSeq := EncodeScalarValue(vs[i]); unflattened := [next] + unflattened; @@ -292,12 +292,12 @@ abstract module DafnyStdLibs.Unicode.UnicodeEncodingForm { ensures EncodeScalarSequence(vs) == s { var parts := PartitionCodeUnitSequence(s); - var vs := Seqs.Map(DecodeMinimalWellFormedCodeUnitSubsequence, parts); + var vs := Seq.Map(DecodeMinimalWellFormedCodeUnitSubsequence, parts); calc == { s; - Seqs.Flatten(parts); - { assert parts == Seqs.Map(EncodeScalarValue, vs); } - Seqs.Flatten(Seqs.Map(EncodeScalarValue, vs)); + Seq.Flatten(parts); + { assert parts == Seq.Map(EncodeScalarValue, vs); } + Seq.Flatten(Seq.Map(EncodeScalarValue, vs)); EncodeScalarSequence(vs); } vs @@ -324,12 +324,12 @@ abstract module DafnyStdLibs.Unicode.UnicodeEncodingForm { return None; } var parts := maybeParts.value; - var vs := Seqs.Map(DecodeMinimalWellFormedCodeUnitSubsequence, parts); + var vs := Seq.Map(DecodeMinimalWellFormedCodeUnitSubsequence, parts); calc == { s; - Seqs.Flatten(parts); - { assert parts == Seqs.Map(EncodeScalarValue, vs); } - Seqs.Flatten(Seqs.Map(EncodeScalarValue, vs)); + Seq.Flatten(parts); + { assert parts == Seq.Map(EncodeScalarValue, vs); } + Seq.Flatten(Seq.Map(EncodeScalarValue, vs)); EncodeScalarSequence(vs); } return Some(vs); diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeStrings.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeStrings.dfy index 4af0f9b3b7f..584dd68cd59 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeStrings.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeStrings.dfy @@ -20,9 +20,9 @@ * Then define a refining module for each `--unicode-char` value you wish to support, * each of which imports the appropriate implementation of AbstractUnicodeStrings. */ -abstract module DafnyStdLibs.Unicode.AbstractUnicodeStrings { +abstract module Std.Unicode.AbstractUnicodeStrings { - import Collections.Seqs + import Collections.Seq import opened Wrappers import opened BoundedInts @@ -32,7 +32,7 @@ abstract module DafnyStdLibs.Unicode.AbstractUnicodeStrings { function ASCIIToUTF8(s: string): seq requires forall i | 0 <= i < |s| :: 0 <= s[i] as int < 128 { - Seqs.Map(c requires 0 <= c as int < 128 => c as uint8, s) + Seq.Map(c requires 0 <= c as int < 128 => c as uint8, s) } function FromUTF8Checked(bs: seq): Option @@ -42,7 +42,7 @@ abstract module DafnyStdLibs.Unicode.AbstractUnicodeStrings { function ASCIIToUTF16(s: string): seq requires forall i | 0 <= i < |s| :: 0 <= s[i] as int < 128 { - Seqs.Map(c requires 0 <= c as int < 128 => c as uint16, s) + Seq.Map(c requires 0 <= c as int < 128 => c as uint16, s) } function FromUTF16Checked(bs: seq): Option diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeStringsWithUnicodeChar.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeStringsWithUnicodeChar.dfy index 552373106b6..7b73339301d 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeStringsWithUnicodeChar.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/UnicodeStringsWithUnicodeChar.dfy @@ -8,7 +8,7 @@ * defining functions for converting between strings and UTF-8/UTF-16. * See the `AbstractUnicodeStrings` module for details. */ -module DafnyStdLibs.Unicode.UnicodeStringsWithUnicodeChar refines AbstractUnicodeStrings { +module Std.Unicode.UnicodeStringsWithUnicodeChar refines AbstractUnicodeStrings { import Base import Utf8EncodingForm @@ -53,32 +53,32 @@ module DafnyStdLibs.Unicode.UnicodeStringsWithUnicodeChar refines AbstractUnicod function ToUTF8Checked(s: string): Option> ensures ToUTF8Checked(s).Some? { - var asCodeUnits := Seqs.Map(CharAsUnicodeScalarValue, s); + var asCodeUnits := Seq.Map(CharAsUnicodeScalarValue, s); var asUtf8CodeUnits := Utf8EncodingForm.EncodeScalarSequence(asCodeUnits); - var asBytes := Seqs.Map(cu => cu as uint8, asUtf8CodeUnits); + var asBytes := Seq.Map(cu => cu as uint8, asUtf8CodeUnits); Some(asBytes) } function FromUTF8Checked(bs: seq): Option { - var asCodeUnits := Seqs.Map(c => c as Utf8EncodingForm.CodeUnit, bs); + var asCodeUnits := Seq.Map(c => c as Utf8EncodingForm.CodeUnit, bs); var utf32 :- Utf8EncodingForm.DecodeCodeUnitSequenceChecked(asCodeUnits); - var asChars := Seqs.Map(CharFromUnicodeScalarValue, utf32); + var asChars := Seq.Map(CharFromUnicodeScalarValue, utf32); Some(asChars) } function ToUTF16Checked(s: string): Option> ensures ToUTF16Checked(s).Some? { - var asCodeUnits := Seqs.Map(CharAsUnicodeScalarValue, s); + var asCodeUnits := Seq.Map(CharAsUnicodeScalarValue, s); var asUtf16CodeUnits := Utf16EncodingForm.EncodeScalarSequence(asCodeUnits); - var asBytes := Seqs.Map(cu => cu as uint16, asUtf16CodeUnits); + var asBytes := Seq.Map(cu => cu as uint16, asUtf16CodeUnits); Some(asBytes) } function FromUTF16Checked(bs: seq): Option { - var asCodeUnits := Seqs.Map(c => c as Utf16EncodingForm.CodeUnit, bs); + var asCodeUnits := Seq.Map(c => c as Utf16EncodingForm.CodeUnit, bs); var utf32 :- Utf16EncodingForm.DecodeCodeUnitSequenceChecked(asCodeUnits); - var asChars := Seqs.Map(CharFromUnicodeScalarValue, utf32); + var asChars := Seq.Map(CharFromUnicodeScalarValue, utf32); Some(asChars) } } diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Utf16EncodingForm.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Utf16EncodingForm.dfy index ed46cbd1fdb..9892385703b 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Utf16EncodingForm.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Utf16EncodingForm.dfy @@ -4,7 +4,7 @@ *******************************************************************************/ // Definition of the UTF-16 Unicode Encoding Form, as specified in Section 3.9 D91. -module DafnyStdLibs.Unicode.Utf16EncodingForm refines UnicodeEncodingForm { +module Std.Unicode.Utf16EncodingForm refines UnicodeEncodingForm { type CodeUnit = bv16 // diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Utf8EncodingForm.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Utf8EncodingForm.dfy index 7508abc395d..795994d89cb 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Utf8EncodingForm.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Utf8EncodingForm.dfy @@ -7,7 +7,7 @@ * The Unicode encoding form that assigns each Unicode scalar value to an unsigned byte sequence of one to four bytes * in length, as specified in Table 3-6 and Table 3-7. */ -module DafnyStdLibs.Unicode.Utf8EncodingForm refines UnicodeEncodingForm { +module Std.Unicode.Utf8EncodingForm refines UnicodeEncodingForm { type CodeUnit = bv8 // diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Utf8EncodingScheme.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Utf8EncodingScheme.dfy index 1d886dec31e..eee8c8c433e 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Utf8EncodingScheme.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Unicode/Utf8EncodingScheme.dfy @@ -18,11 +18,11 @@ * that states lemmas/conditions about Serialize and Deserialize * which refining modules would prove about their own implementations. */ -module DafnyStdLibs.Unicode.Utf8EncodingScheme { +module Std.Unicode.Utf8EncodingScheme { import opened Wrappers import BoundedInts - import Collections.Seqs + import Collections.Seq import Utf8EncodingForm type byte = BoundedInts.uint8 @@ -32,7 +32,7 @@ module DafnyStdLibs.Unicode.Utf8EncodingScheme { */ function Serialize(s: Utf8EncodingForm.CodeUnitSeq): (b: seq) { - Seqs.Map(c => c as byte, s) + Seq.Map(c => c as byte, s) } /** @@ -40,7 +40,7 @@ module DafnyStdLibs.Unicode.Utf8EncodingScheme { */ function Deserialize(b: seq): (s: Utf8EncodingForm.CodeUnitSeq) { - Seqs.Map(b => b as Utf8EncodingForm.CodeUnit, b) + Seq.Map(b => b as Utf8EncodingForm.CodeUnit, b) } /** @@ -61,11 +61,11 @@ module DafnyStdLibs.Unicode.Utf8EncodingScheme { calc { Serialize(Deserialize(b)); == // Definitions of Serialize, Deserialize - Seqs.Map(c => c as byte, Seqs.Map(b => b as Utf8EncodingForm.CodeUnit, b)); + Seq.Map(c => c as byte, Seq.Map(b => b as Utf8EncodingForm.CodeUnit, b)); == // Compositionality of Map - Seqs.Map(b => (b as Utf8EncodingForm.CodeUnit) as byte, b); + Seq.Map(b => (b as Utf8EncodingForm.CodeUnit) as byte, b); == // Simplify map - Seqs.Map(b => b, b); + Seq.Map(b => b, b); == // Identity function b; } diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Wrappers.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Wrappers.dfy index 30da42efb59..dbe4fee46d4 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Wrappers.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Wrappers.dfy @@ -12,7 +12,7 @@ All three of these may be used with `:-` as Dafny failure-compatible types The module also defines two forms of `Need`, that check the truth of a predicate and return a failure value if false. */ -module DafnyStdLibs.Wrappers { +module Std.Wrappers { /** This datatype is the conventional Some/None datatype that is often used in place of a reference or null. diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIO-notarget-java-cs-js-go-py.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIO-notarget-java-cs-js-go-py.dfy index 63395a682cb..b6473d8491d 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIO-notarget-java-cs-js-go-py.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIO-notarget-java-cs-js-go-py.dfy @@ -13,7 +13,7 @@ * * File path symbols including . and .. are allowed. */ -module DafnyStdLibs.FileIO { +module Std.FileIO { import opened Wrappers import FileIOInternalExterns diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-go.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-go.dfy index d82172e81c7..439a8d5d2e3 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-go.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-go.dfy @@ -12,9 +12,9 @@ module // across multiple Go files under the same path. // But it makes debugging the translated output a little clearer. {:compile false} -{:extern "DafnyStdLibs_FileIOInternalExterns"} +{:extern "Std_FileIOInternalExterns"} {:dummyImportMember "INTERNAL__ReadBytesFromFile", false} -DafnyStdLibs.FileIOInternalExterns { +Std.FileIOInternalExterns { method {:extern} INTERNAL_ReadBytesFromFile(path: string) diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-java-cs-js.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-java-cs-js.dfy index ee5afc4b546..0b0ef4dda4a 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-java-cs-js.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-java-cs-js.dfy @@ -6,14 +6,14 @@ /* * Private API - these should not be used elsewhere */ -module DafnyStdLibs.FileIOInternalExterns { +module Std.FileIOInternalExterns { method - {:extern "DafnyStdLibsExterns.FileIO", "INTERNAL_ReadBytesFromFile"} + {:extern "StdExterns.FileIO", "INTERNAL_ReadBytesFromFile"} INTERNAL_ReadBytesFromFile(path: string) returns (isError: bool, bytesRead: seq, errorMsg: string) method - {:extern "DafnyStdLibsExterns.FileIO", "INTERNAL_WriteBytesToFile"} + {:extern "StdExterns.FileIO", "INTERNAL_WriteBytesToFile"} INTERNAL_WriteBytesToFile(path: string, bytes: seq) returns (isError: bool, errorMsg: string) } \ No newline at end of file diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-notarget.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-notarget.dfy index 2d883d601e2..1069b18eb8a 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-notarget.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-notarget.dfy @@ -6,7 +6,7 @@ /* * Private API - these should not be used elsewhere */ -module DafnyStdLibs.FileIOInternalExterns { +module Std.FileIOInternalExterns { method INTERNAL_ReadBytesFromFile(path: string) returns (isError: bool, bytesRead: seq, errorMsg: string) diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-py.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-py.dfy index 47f0a9efec9..a5582df662e 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-py.dfy +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-py.dfy @@ -7,9 +7,9 @@ * Private API - these should not be used elsewhere */ // {:compile false} is necessary here since otherwise the translation to Python -// will create a DafnyStdLibs_FileIOInternalExterns.py source file as well, +// will create a Std_FileIOInternalExterns.py source file as well, // which the embedded version can't easily override. -module {:compile false} DafnyStdLibs.FileIOInternalExterns { +module {:compile false} Std.FileIOInternalExterns { method {:extern} INTERNAL_ReadBytesFromFile(path: string) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/randomCSharp.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/randomCSharp.dfy index cdd56b5d08f..8760c6dadbe 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/randomCSharp.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/randomCSharp.dfy @@ -16,7 +16,7 @@ module RandomCSharp replaces DfyRandom { module Interop { import opened CSharpSystem - import opened DafnyStdLibs.Wrappers + import opened Std.Wrappers function {:extern} IntToInt32(value: int): Option ensures var r := IntToInt32(value); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/randomJava.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/randomJava.dfy index e8876088452..c717d397dbb 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/randomJava.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/randomJava.dfy @@ -17,7 +17,7 @@ module RandomJava replaces DfyRandom { module Interop { import opened JavaLang - import opened DafnyStdLibs.Wrappers + import opened Std.Wrappers const int32MaxValue := 2147483647 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/wrappers.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/wrappers.dfy index d37f1f5a6a4..e328390a1fe 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/wrappers.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Inputs/wrappers.dfy @@ -12,7 +12,7 @@ All three of these may be used with `:-` as Dafny failure-compatible types The module also defines two forms of `Need`, that check the truth of a predicate and return a failure value if false. */ -module DafnyStdLibs.Wrappers { +module Std.Wrappers { /** This datatype is the conventional Some/None datatype that is often used in place of a reference or null. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514.dfy index 7e456ec8e7c..71ffa8a94e4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514.dfy @@ -1,6 +1,6 @@ // RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --standard-libraries --relax-definite-assignment -import opened DafnyStdLibs.Wrappers +import opened Std.Wrappers trait Foo { function Bar(a: C): (r: D) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514b.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514b.dfy index a672014f6a4..876880c5298 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514b.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514b.dfy @@ -1,6 +1,6 @@ // RUN: %testDafnyForEachCompiler "%s" -- --standard-libraries --relax-definite-assignment -import opened DafnyStdLibs.Wrappers +import opened Std.Wrappers trait Foo { method Bar(a: C) returns (r: D) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514c.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514c.dfy index 5bfbd71ce2d..cb5574214c2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514c.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514c.dfy @@ -1,6 +1,6 @@ // RUN: %testDafnyForEachCompiler "%s" -- --standard-libraries --relax-definite-assignment -import opened DafnyStdLibs.Wrappers +import opened Std.Wrappers method id(r: T) returns (r2: T) { r2 := r; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue1495.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue1495.dfy index 87c6035eee0..b219fa5715c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue1495.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue1495.dfy @@ -1,7 +1,7 @@ // RUN: %verify "%s" --standard-libraries:true > "%t" // RUN: %diff "%s.expect" "%t" -import opened DafnyStdLibs.Wrappers +import opened Std.Wrappers datatype Bar = Bar(i: string) function ParseBar(s: string): Result { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/StdLibsOffByDefaultInTests.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/StdLibsOffByDefaultInTests.dfy index fc7e5c107ce..e74ec08c65c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/StdLibsOffByDefaultInTests.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/StdLibsOffByDefaultInTests.dfy @@ -5,7 +5,7 @@ module TriesToUseWrappers { - import opened DafnyStdLibs.Wrappers + import opened Std.Wrappers function SafeDiv(a: int, b: int): Option { if b == 0 then None else Some(a/b) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries.dfy index 60a5cfe950d..e25846108a1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries.dfy @@ -7,7 +7,7 @@ module UsesWrappers { - import opened DafnyStdLibs.Wrappers + import opened Std.Wrappers function SafeDiv(a: int, b: int): Option { if b == 0 then None else Some(a/b) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy index 81b33b7f02e..2256ae6f3d0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy @@ -17,7 +17,7 @@ module UsesWrappers { - import opened DafnyStdLibs.Wrappers + import opened Std.Wrappers function SafeDiv(a: int, b: int): Option { if b == 0 then None else Some(a/b) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy index eecb3119553..b1d1c38d18c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy @@ -6,5 +6,5 @@ // RUN: %testDafnyForEachCompiler "%s" -- --standard-libraries:true module UsesFileIO { - import DafnyStdLibs.FileIO + import Std.FileIO }