From c45c1748d8aa3100c2d327658e253abf7ae78e7f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Feb 2014 16:15:44 -0800 Subject: [PATCH] refactor(builtin/kernel): reorder congr1 arguments Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 11 +++++++---- src/builtin/num.lean | 4 ++-- src/builtin/obj/kernel.olean | Bin 51327 -> 51377 bytes src/builtin/obj/num.olean | Bin 38268 -> 38268 bytes src/builtin/obj/optional.olean | Bin 6740 -> 6740 bytes src/builtin/optional.lean | 4 ++-- src/kernel/kernel_decls.cpp | 1 + src/kernel/kernel_decls.h | 3 +++ src/library/simplifier/simplifier.cpp | 2 +- tests/lean/add_assoc.lean.expected.out | 6 +++--- tests/lean/bad_simp2.lean.expected.out | 2 +- tests/lean/find.lean.expected.out | 2 +- tests/lean/simp10.lean.expected.out | 2 +- tests/lean/simp17.lean.expected.out | 4 ++-- tests/lean/simp24.lean.expected.out | 2 +- tests/lean/simp26.lean.expected.out | 4 ++-- tests/lean/simp29.lean.expected.out | 2 +- tests/lean/simp3.lean | 8 ++++---- tests/lean/simp3.lean.expected.out | 6 +++--- tests/lean/simp31.lean.expected.out | 2 +- tests/lean/simp33.lean.expected.out | 2 +- 21 files changed, 37 insertions(+), 30 deletions(-) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 5983dcec61..953247847b 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -138,14 +138,17 @@ theorem symm {A : (Type U)} {a b : A} (H : a = b) : b = a theorem trans {A : (Type U)} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c := subst H1 H2 -theorem congr1 {A B : (Type U)} {f g : A → B} (a : A) (H : f = g) : f a = g a -:= substp (fun h : A → B, f a = h a) (refl (f a)) H +theorem hcongr1 {A : (Type U)} {B : A → (Type U)} {f g : ∀ x, B x} (H : f = g) (a : A) : f a = g a +:= substp (fun h, f a = h a) (refl (f a)) H + +theorem congr1 {A B : (Type U)} {f g : A → B} (H : f = g) (a : A) : f a = g a +:= hcongr1 H a theorem congr2 {A B : (Type U)} {a b : A} (f : A → B) (H : a = b) : f a = f b := substp (fun x : A, f a = f x) (refl (f a)) H theorem congr {A B : (Type U)} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b -:= subst (congr2 f H2) (congr1 b H1) +:= subst (congr2 f H2) (congr1 H1 b) theorem true_ne_false : ¬ true = false := assume H : true = false, @@ -621,7 +624,7 @@ theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b theorem not_implies (a b : Bool) : ¬ (a → b) ↔ a ∧ ¬ b := calc (¬ (a → b)) = ¬ (¬ a ∨ b) : { imp_or a b } ... = ¬ ¬ a ∧ ¬ b : not_or (¬ a) b - ... = a ∧ ¬ b : by simp + ... = a ∧ ¬ b : congr2 (λ x, x ∧ ¬ b) (not_not_eq a) theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b := (not_implies a b) ◂ H diff --git a/src/builtin/num.lean b/src/builtin/num.lean index 8b73e7ce2d..79e6d4216f 100644 --- a/src/builtin/num.lean +++ b/src/builtin/num.lean @@ -446,7 +446,7 @@ theorem prim_rec_thm {A : (Type U)} (x : A) (f : A → num → A) calc prim_rec x f zero = prim_rec_fun x f zero (pre zero) : refl _ ... = prim_rec_fun x f zero zero : { pre_zero } ... = simp_rec (λ n, x) faux zero zero : refl _ - ... = x : congr1 zero Heq1, + ... = x : congr1 Heq1 zero, have Hs : ∀ m, prim_rec x f (succ m) = f (prim_rec x f m) m, from take m, have Heq1 : pre (succ m) = m, @@ -456,7 +456,7 @@ theorem prim_rec_thm {A : (Type U)} (x : A) (f : A → num → A) calc prim_rec x f (succ m) = prim_rec_fun x f (succ m) (pre (succ m)) : refl _ ... = prim_rec_fun x f (succ m) m : congr2 (prim_rec_fun x f (succ m)) Heq1 ... = simp_rec (λ n, x) faux (succ m) m : refl _ - ... = faux (simp_rec (λ n, x) faux m) m : congr1 m Heq2 + ... = faux (simp_rec (λ n, x) faux m) m : congr1 Heq2 m ... = f (prim_rec x f m) m : refl _, show prim_rec x f zero = x ∧ ∀ m, prim_rec x f (succ m) = f (prim_rec x f m) m, from and_intro Hz Hs diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index c12e75b9bb4620a13230b1a81909c22c5958979b..67451cdabfc4521935c3982885a894846f6415f1 100644 GIT binary patch literal 51377 zcmcJ237DNlmG-yX+xOn?Mv%>bxP)jYQ3!%4aS&y32@+6I!3}#!IybGI?vU<;AUtD6 zA>%g8XxLm(5JkiV#T6G67#D;QHSWR;Ad4dk3gQ;jIq&<{cE5W&0srUE^Q8Jz)u~gb z&Q{A;-*=}c$494DO-znw?q9xsYGT9qx|#8;cv+U`R%%HxHa(lI9AA|cFFkeb_{*|> zU%^KGNQ*VE8(z0=CMyhWbp7OPwqbN#RvbA!J!#lP%SSh6#p-qAt0uE%aRiGD7|jZR zgGfpyN3U6nzggY>=Q(>FKRGnX(FFg>W--RLd8ux)28vrqa)RWmBshT520LNC^qn+; zogX(nJ32ctJq4`1I4lFh2a%g*HoH12I+%_eJQ4W2AQ4eO>ThR&;)3<%6G#n1^2nZp zM*uTNFRRB-9-ecgY#2KP-`Sw@5FmvpE|~6$dNHsYK(Vzuz=n81zgZ?ao|i{ji4*zk zy7lA2P$$h|qq0bw>|;-YNI1ABU<|YCCN@lrPO4;&>#EU7 zGc^2bcF-?9-n@Kta$?l1>bAFjka$BO{~`4;Pj)$F28w?R8qPe7ptBPcFYeUvH6KG^ zwupT1BMQ^&XpJbRP!@2E^O#-#L_^h+?)d#2&jSuRq zy6w%ECUvy>(W#X{%=Qms3VetMKSc7eq?6vz5Xmhd9}6pd9PnyYg8Cty?QVPXhm$(; zF|lUt{SX>ajC*m|J{vqxIFtgD#mp~7jojlI0OcP41n_V&Rz}O6hth`U@es=t z&POIztwLQdp~z`aNn;Wdosxd${?DSM_aa}1R#bG`=Cf4`8q48Y;~1-Kx=HRJuB;@x zG)E2M2$VJ(#j+{k9!o3`n3|p)o|u|lHy!CTi)ElIrwt{vMR*OqpU>H zYIJO7{koMMqz(i=0`oGmmMuY60)IY0QDu+f^=OnXk-z~4DL>CLKK5^%n3E+ zDJ4e%i}W!dBDF3Dc#?$UV~evn7D^+UUD(60O?)T2m^Yl*ttO+Bo=_I!;sk`VM#II! z22}y8$VQsQsrZ}CgPvr8h|A=XNyb~H#Afj#RA&oJmIo^0kiZaS z8wapBSOm*RvxKf0S-pceqw&gK49X1(;MD*nyORJe9%45q0M0Z|Jc=-j8=$;qHi+M1 zY>11-CjKpr$|pxO%r^TPM!otPi6D7fN(9ncVwNj@+fQVtFoi5@lNw!7tayKXja8aI zg0mIVX56D|rxmHr@FB;1!EtG%No*;+LuE@eU{JA6kjUKu1*2bS8P|ubzDuxGF*Kr{ zC;<|k$5Fl(q$P&eMQ{?Jbg~BE7771VfU|kDr85DNMbZh}O<1u6FuhLxjRjUk=Ugp; zKoUA6O%j`C6+zm&+>=2Zp+vgfB3Yrolo65f`oJ2hlN-#dK|U3>|7$^R4x&% zM_&Rr05rdI+%UKV|AEfc?U*e&S4`WKH9iYJavdsQQjT1ZF=)_|hI$n$XwjRSL+JN3 z@9%8*X_@AfoIDaF>Ja6s=ig3$i2LzW&)V=8M=%%&Z@qK`=T32w7Z~``*n7 z<5WQ_wSZ;(FqDuB3)I$$q+J+|8VI$K%p(#TwSCubvhrGP{}620IejJjc`{qb+~O*y z;R5;hg57>U4D1J5f4+%}_d0sribVYblDK^LZ?lrp_kQY{-YXwD8p00+D%Qy=q4C>P=cIh=3B!I)Ot)YV=G2MV@)Wbh_7HtSwxB^yCa zb}`Z{+FD$G5M>IKI+mL{QAGjH75GKZJzq9IF0wWVzySt8i>+c}@lMjr7!v ztbD^-)f(??;gOmI?j`P$ObX<`4Rj3uPXup?;H?HahHnG-PO~I8BSqm$0%$~{ zfqyuu=ihjLc#?(|bFB*Q0BMQ!&IsNW!Cx9k)@bC$Z(x$nmDov)8x%z_h}(^VXLWXZ z2WR5&ef%3lqJ`S80V=5e2B6k=_W;!NbT7a`$&BrSDzf{uF?%F1=A3Wuwz`BtJGf6L z8>uAhxZ`5nTIH8hE58GEad;m(Qh5g0q91k`D%{+wN6MgmBpqUIQ z7ILs;l2dvPL@6{UOoir{X{FGdg57FdABeK-j>H$JP`WLX|^2Nc<3G5+y;((y*UQ zGPq%WD`l_~_>v4B0Z=m78K7ja3qZ*LAtRRzc17t!+bKpFaJUo%x(+Mb904i}cl_kp zuER&gKZXD?wL99=S@JyqekwXCAU9QqI3mwy4ZAFP(_UIBu9 za*#g?pt_|*uh1FhQ7ATX`Dq}T0Eou*Rp*fRvRzjB)?vqi|#A=o+k6)`PsnGYIKjd&B^tSZ1?v6o101VJHkO&r#;$vFvGo(AI3_E;u{ zU+)$RJ6X+D3nJ3zHvwk!(_+3s#X=-Q;_5WisYyAya;04fKmiXx^2byQ9*;FC_{M+E zp`*lZCL)!LQG6^CIUr@$rj)UQlF^G|GZsNN1^D~ev2aN?uYb|UjK&@Y~g zRN-?!fMR2RfMP=j{^aujD=eN%pE)%S1S=u8ej{U9)<%h0z?7 zK)0$ao`QCYs+_nLUJkOt;whE>^|-SEeu@{c8IsT^D8<;q9fb8b$Fgi{bS&A>E(IY? zGO{rWfp#f=o^JKUn8F=7&gKmi%Z6uGPoI*xC`yE-%cXeJ#q#6-iJ9VvW8cevSqc0%2~&X6{^a=*1a5JtipZ`9P8dLQ3d= zd&=4jG8!(o2kMDISm1G>$3r=tA~w`Nl+m;QV}P&z?LnoxyAj+i=x7Do>qvsyfwMU$ z<`S(#U z0XPaLKOK{C=_c>_H>*)07W*3BHk8dGp(cYyUWgJGhU|*j`t*S%0+1gmg|1~18GR*4 zX?(9TsQ5UK<#Ld7uAx||Dfw^}8#m7Sk+&yQF1v(6J|BgQl>SLu{t7FRy6}K;eB&I? z{Vh`A-%?|EjKj@ePdC^FrA;JlBr@L-fa09E0!d*hhX(EEug5%8e6kmr>cdphhG>c_ z7a(<3V3Mc2i>pKmRaYVTYK7=lD6fvg+b$Bv^Xp)r`O_IhC(tIuI#mmV6 zwKTpJpu_UM#_Z`PS;n-CHWRkBSQJV|*lo?h#<9KF;BAF`JvtN{8vq^)@_O-3`1Rr(RK8hl9RYdp$rc=uQKeNa%3n{oW%xT&HiG z`drLMJ^TuPGshbF=gyh@Q>;va#o-*<3v+k^*CCD|fp}aJ8GR&bq{=q{6r-B}>fWyQ z4cQ~vgnNL_&JYR`>#knDSRT8gq?xF{H=+|>$tf$_4mVZAE}KB*P7n8llOcs^LU$JF zDK#Lgi!%Vy5OZprSS6_uYY#5gjpUrSDdnC17&G5Wp4iQOAT1UDD?mx^%>YY?D1Qq; zEh65E{8p_|8D@EMnFWn)wt7Dq;(DhY{Dy5|Rd@cug{}{Qm7JmIPRKqIMj{c zDKp8!T+JD2*PJ+Yi6UCJbenjqQJk5XUSVB`h!GW$cC(j)JNZR-v%K z3Hh`WMbS2rqHPaHMLT&+yN#_lr*I-k=d4&I!3zr=NGJaRP)73(6l!m9Ho&J+mDrG% zhlcAW4bMlz^RdVfwDHCwt2|6SCjDAz407eOcZ8n^2K0_b49z*!lRnn4`89G<@&>sQWXjnl$oc!#{LhE{gXa<4u16S);2D) zouQ3_A}-mxnKl|4+#tJ--7xyQxxfnZ51>jD%EbiZgmRtbOS>hz4CUE%lkEuoyHgGkwp@f z<4{N_tc<$c7$rj=R@@*u^5sVK3n^%5iV2hgeNka0pxge*R()uawP_*{XL%a(@_4pn zN3;{5OF~il>XMyL`0>p|E;WcSQei_{376^{eX;M7{%1FZw0tSf@1&L~>|hXLm2$(F z(~*2Gbg2L(Nzhz49*F~d#6eYTw!|c%DHu0xdr$L}C558|L(8v3L!MW1JyyO8d2qgPIuZmkLMxCNFJp91J5mM&v< z5DU?2Ci)c3;{7zL>p@Y|#tjktFM^9Pgd9_pp&+5xeuAZ!A+P8!Bde~oE~*w>RxS8K zwcyLug0EEzuBjG$qgwE-YQeW*)$Y>sL1B#-Cs*6XYM*tTL5v4F8rI>|jToiG^W6x3 z51=NH?*m-IsbW4rhBF>6@petQF-l!k$jd<50bdgItK08bxmy$9=x>fiL9iN~>Sf%8 z(dM**{{g6r^B)o&`2V{eaMG!cpp2D{g4A+t1Ycq zWrb=Wr7eBGe+?vDZOFS-VU)4>0yBw%d-Ypxi%2w$Ah24$ z7yaBJIT`|3ar4hF07gTo?XD^X{~E6MIk(<~;W_cGH zS0;$sW30^arP+|H7#%6O+3+^BQ*4JPY-e#0g}|9uJNo}c>qH1-%b(QLI0GiGs43j( z*`L!yd!+#h$4g;5ivsc^Y%n2yenWmb=gHbrtgt4|&{^&AKvGN1lfOhk6hif_MRKSW zQWV0mXrfN<1(*n7sj8eMEQPsdXCmPOI5CPPD3s;WC@BCHZeK{k@j`l-GxA>(iARtQ zAzQj1Y$-zgK7tPrgxE?<6`GnMkJ{roHQ$87?M=;Ft8?T{)qHH|um|d0 zvPTF`yEy@QKY`RvSime2bf)DOI4$n>z4i7Ow0IJdW6@WU1Jql7JU8Gn>(~wwT^yqc zPk1Pgg7S&-@Kr9r5wTMq4|ww3n<6g^(xfod2f?@+t*!Q6LBy`h4S%R=dRwKS$f^ZJ zwV=;)nZD{Djzkm*Ac>^}xo~q1YlX!Cs^~ezAVH{C$Lk0RwJAS}jRwWUEPU-2}`LtL}JS&kYBwC?zxp9{YB5$klw5ZbCw0dO}0JwHKgtKO~!g zs7ghts(&EiM`$@Ak?C=g+;$Gt_`sV1eTC$k(aA5s>N zLIa*k7HoDBY_-@6rQ&~YgKBSQ>7xOjr5X4Yz_16M#qk8(6${^;UVp-{^4-|)iwg#y_rpQ&1yPiQ&9y1nfA9JbYn~pOL)BB z2Mg4aH*`#<1{_-qNd+Av!G`SPN zZ4b>L#VA@wzr+K(xK&rw$F zJ$aB%0u%|QTiQJ#ttVh7QGT(>zX^++@x&erZUPHVReQK$_2 zynIsQnv<9F%iE*gI=RfX05JmLEu#X$?qy6k=h$vgk>Eiq2`v^2H=@WL(PBlJtwy4E z`DA65t^J6)c^0Z2fZjcmSiP8fWS}MbAgGEi^ZG+s65kTfz zF+>WY&0p`w0Ov0AtU8K~-NFlVgVcIO9G2#zVe}`iM*zxzAoAK3kyVVfc1=_u+h*sX z0mT6BAb#VZ(+)>?vgPX#t{QMT<&{-`O;DD-Mlf@*jkGXCP|NhT zF}XzNdA~Qmm6q!aU+ee*tDqwqTYX8B3>h`bO(!u>0t{Tzn}-~G;5NG0fV{K?3vy0G z+$Lq0zZMvE42k|esjOrGxO3T&((m#qRw8JuLqj{|EiElLak`Kf_1(6r`YGPRd1CLT zAaGxtW=S#|fl!=x*IPyrXVvt&(aFi-ha@d)RL6SKhG|LhF90Q(HyY$5^CpyXH(!V7 ze1l?{J{7^mZUEX6mJHSLg`x~_|^!% zErM@1u+Hz$6lVcEXOX4FCxM__zH~t_Qa^VAsy@Xklg02DAp2f}C9Z)%^$R!^Xbe8q zaQ5Hka~u^Zz7J$HCXwMf*#v{ID$mSM^v$q(ptI)7*rjmM$oJb>F%ptjVp^8}BC^_aqFw?drj^~<+#S!WFE28Ik_9JJk09r z7a+L^$sF#0st+K6=w$qHD4M>wtLq*L8eQU@1Kdj`ml?$Axc=4c=>hnVZ@0gpy~Mvg z-HA0iQ>tE&#YpNuMe?JHc}aY|H3R%FAz|>i3eXJ;kX~yEO}74ZWWVD>^S@dyyfixD zqjPfbyMyTLqAsJ6y9*S9Gv^5$C50faxV|I_fZ&TG0&@La46C@%5*MAJbq7Mh4uo(V zhzL;s4Vzs8@LtNBwi8d%*h3nfZ-!RIG((1>Gg!zrfyzY?ngThl`3#Hic2$=^1q0jB ze^)R?n-5u%b*a50%t9vh4^>pJ$by=WAd!_;a5#5tFBGE{tz7o-;U`#L-`;Ja=FiA0 z{*qLQ!cQRiRHY}_Hz(lw=TQB5peb`X13KebsCyutGcaZz1`c zC7J)kNb!ElbO#+v*Z+LbVDBU^6& zd4;gtNZ!AILXGIk2!1hw2>1@+%Lci%Djni%XsqwaDCGi*Bim$Ij;v$8tv+H2uBAsT zo6#tY{qvUT8vDbZHQY0+O-8K#Yd1{*zSokzgE{!G8R*7#bp$czy3%VS_@4&$J%`P{ zVW3R~h+VX{?%|`EJteS6AzFW^m{5>y9&47}@>mwi+4VeQ9^Lj9b?ZqJe3GCjm9qZbwY zKuhsm6l#3mi{SSoNV^om53IC)4#mQ_&+S&Kn5H2V??7A5k+AFH4an{nj9oPsps9N#6>Jgj0+J^)oAVLj8FJZ;Bwrqoolhn7&hcn0Vi7ttJ&8kB`{$0#J(L zOIAxekczf0@~fgvIdd~5Ig?_r#-CUp-GcjvTxlf*^b2q;0o@+KJ0f^z1n)Ai!VH9{IXnxgW4000+1m@$ePaXuSOOWVd#@zrlf?pFH zvb4Chsq<=Hq2#`+@4b$rz6+sPEn&%5^(Fy`*Jcb`I^^f%dZTYL%xsHCA44wV)1mC* z=-m`Rn|biAxp5P?)O9x1qbW3!l}Ip=b{yew(%NJ-Y7WQS-W3LTFzDEzEiHayNf{sT zWScBczO^GoVE2;?_ZnxSo>%#G^{UEZl{@0|=~+qBsp9)bzlfi6zM(FL-(x-ZT|}<` z2ri`AKSdBLy1w^7e0lsx1urZ1U8G04zXGy5a03*)hp{g{B;U?`m0)!49Ug}1#OOHN zi?s*Qg}c?`j4tB@#WmnJy&|sfX>_E!1r(}AhXH06+kba4nV6eU2=wxGfD*lNK2D9) zs{1ha(U3bV(+bPef_XY~q}pj@ZL8O2q{|Y6&ALXwl+F54ev^v(tCe@ZP6BMmgtLZR zOAlOSZL9$sG`XY)_<|b%xg07#@vCeeZzX|y8$eh90nDty_~=n5WZ2d zHNGp}*2+FBb_ex{aCTO}AN%NDv{Mtyfjt(KBB?UIl>_KN>W{VmeZQ?D1%s|lq5k)%kGrmHspagt6AI5mlAghZrulqSRX^FI@1qp`sB_kU zarDs(=`tlct4xC8)eLwenz_dmv~gM;+7++ynsmb3fjSdO$ocsgu-uvSsbp;DoG2fO z4#uQe1N#sf8g=Tl)KEAzP$E8ll#f6o#SiNncT$5t`+ z4Z+TS{V0eb94AW^95vR$>Ag_JSPZ6Ii1BK!plj>x28I)A5U$lgQhvikrAd|H!<{gS zepEX>UQc!~Lutv#H|KclqI`ofD@;g@7kkXc@zt81^l6Y>za&A7x|!oxHb|kksYhO)pA0n)qd>IXL*YwNom{5qp7Ej>NR@0>CcnnZ6r0#r#*IQU287eb@f=Cl zq>A1*A*nE%Z9zZrII(d&khWl)4eF~ZD6++CFx@kE9Kj|~NfgI?rR&D=on6auP}Vri zti^3dj;-o6cEafcKH7Lm70C*D@uRV!T2s{^O^y+bCklx;DM*sX4UERCkUYPl)l;m{ zjxUgQiM-kqwW^T9F+_veD6Q@bGF7d*Vf608&~@LtBHDtt780#)Fih?B8$64tYL#p~ zG_6u1QwJ6KRPjxjD9FTqet1RWPy_KzS!PvaQ&bt*u(e&Z!tMWM9k z%J|7v>{e0kQiiS6SK60^a5*4+N-iN%R(Y=DocJ&fFUp`T6Aiv|7edQc6w?>@tPA zpgDm{?zqHw*Vhr6R$o5d678^N;a5V{?F;O{8keHJ?U%+|$rP8~TTwBKgwnvG4jJ(2 zc!+$0oyMh66oEbN8aZEL|xo_14sqcWC6hwJSODHpKiW%dosw$`Nz?GCseL=%iRYSUgni4i47Wp7IERTI7gS{q=lslG__*=S=pt*8ujSs#rItfb!_mpv zkf%#EE~IX_Sdfo#HP5S!<#A}0sOjgHZQSG~^YbCg@;fwY}-h}T5M^H33G>~8;5(1}C2p9oNLe>p(82W=&h`~6na_=6YG{R=JY zuf=+4kt=Gs4LZ74&b*i-2W<-DJRk@Qka@}}_)C)~)YwK@-;P3E1ZV5yLFmm^llMn8 z(|KgVXsX+OK!RZy?@{FmrXSBAlJNjp?{11=GE`Ea|~@mRz7Et0hlY+$#=f zBd!7QzISq%JJC6mW)38(GPvXkR?=ZP9ntflc;uXh!-%jMUB;P^_s|;;Kw;%dRLMxj z0m?ZkplBq`M_WyEA1Bo2qZ6TeGmS^u&ZWo^davP3bS}X*=P$Ba9#v|CHlcQLJXOos z4XjXx2*al^Am)2Q#+g1pL*A2XYul`*_KP8;JcUBOi4iy@#IEAIBUWiIkQsReRH`uh zQi6%*Ft_HSPQnVf(ykZRK4FMX6p>CFB)GD~U^tfAgHgH`(l??fQtfyzqG5%l=3!C; zpUF>l1;4|jK)=iT6GmfeT{okeegP7Yu3Rd^^rBDOVcsjlMl0nqI>&^$%6)5N3dVD!guO#|UHflLxbJUAK2k#`lm_W;(0-D1} zYzj}De>S65E`Yq#1OpKaGFX-Deg1Dyh0MSb`tmr z&+u}NZLt+K{oBCJbs$(fJCcpFCn~E$O?`crC0bnthn=agU%IB zT;})MtWi5X-#uW>A?S1jNnG(X9zb4;{c{0oH0J@-YUX@^Ee67`UN54aFa<36t~GEsZHl{u#P6`k?~6r{2N??QvD8V`6`frpMMeZuaCKD<>n z#X^&e=IqY`H>2C@U5-*|{Eg=KUaN3ox&WY*{yuIvH`uGqH0F0yB&`(+?t-@M9IrlEZA>6^a%Zo?ha*nX$o5vRLdYV*B6iEk9@_{%P2x`;d8< zqr=#aLc^?cj(#GFc0tlavKh%pXQAH%T21*e)JqN@2Pgyo1VGK!mmAc)36kS%?c2In zabn2lQHo|)KI4NKx!x@zuR|_wJ0mhzIa*Cc8%UO3;@^jXj~W#}N3LBr{n`V=Hy%2L zgZJo0vsOA8j^Mbzh4xp17x+t-{Pt|Dfqu2cU}&k7+I=X<=IM{5 z#E>N^U4=@4Up1)JN6}mjP`K9sWN^)Hiv3}n$(k=pskLjA(pL59I7p-fMq4z?Af+!` zQIOK=?TJaoWa!O%+#{pry$}gXem7_-DYphVkpD!nhWB+qvWIUN=l7K?lN?5g%K=?AwkKFyU;{Z@}1&rFz9l87S{&m>@yJJ7#qI_HQrDue*{n?|1ltq z{3ihW_yq`kXv+0%#lCSm-|Fp!%~l(J|GmVtVKUh;x-Kim*LM7RIIRe8lxl4cd(ZsG zQp%rM#zZ+eF*=hK-}!8&CnrD4%3?UnAYmgmY=4u{R_XZ#j`^^>e1z7+v-1{@59wG` zL+JMw>({@AjV|n|M$(1bg?NIdyE!Ox6VUvw5z`SC%u7!Nb>Jvb{}QE|b^aHiO}QLI zHnOlR4tFC&1&Opy1SIVP3hsQTW&C2=Se}`fYEO>OPEVzr2jPfe?Ure1i9DSDd7TDx z(HLOtij=aMdyv;a?lnlSua>_>X=A`Eb=-c~Xf(@F7=IDm$wY>A3+fc!s0xV+WnqB7 zv5XczVZAfF(p)SZU~uncD0ZWS!nNq2?g`q$2DBfr#Bq=Hy|ef~8rYgetfBI-2-;{F z6FY<Ct2|}?it!<%?f>0z#V(w7g{?VF<3Pjs_}yYI#1Dn^)=AqHDD&SKV&J)8ud$4s1+!s zP1j&B-Jcw=!q&e5DXbN75$_a~WSbXS(wYRwTcWME5=7EQ!T}P3q=JFeka1!k-8eD5 zW_Wtl@QT&b6DxXuX5e_U5D71OFi7CFmQa-(NZU{o-w1x`3N&GMd@|1&X69LngNC zccEpuRcYMim}=bRnbHwEW4@RQBjA!(qQO{biy$DYY+VKBq?Z$%CFCctF?TO*@BoVW z(*XHTXVtK7fpEDRvG1s)(P{-SVQ(%_`NarD)}~493k*qX0g+kCZsl|g&q-VYAFUG` z1@{~7xbP6)11f7j_Bs7R7Q;V>0McRZtW>=3-*~B|JGoIBAWq*v> zkn!Mu!rcr@=1Pq${>*KhO?Z>N^>b@2hlY6F#6pMz-5;QazXTxXoEjbuXUWAN$g6cz zjLmdf&ASw(sZ-*hoV1mJD5x(N%NAL-I2eUp)U2#^Yal_{2Z<&>ZAF`+4BJk^?nmq? z;aE%hx04J{2h<<(#cqjs(CghuZjY=nApE9+bUTqO(c6ysNdP%+eV&8evy;2oY0Q(d zuFewwd)CnPNn;Zxx)&1aB_4#Q)-OQLO%8x=U5NB3OSH(T9Y_!f8CN6fRW+4?{V&-& z#L!!}p%E;ib=#9l`{5OPDGDVbWOp_J67kLmqD||UsNu`J$(3N>wC+Sgx`%KXnPXD4 zk_r>Q1go{DqHZzj?*cSrzfd~i-^WIQeSyf5)=Gdx15`YtQ7<_BlI0u@RScS~yTC^M zT7WA7*5KRZsC7FJL$v*ufN$4P71lgXUo8{Qi9`*IF6*CO&Zb z9}Pr?-9wOFPA{>eWO8KopqS^dEzSk8gBeI_-U_)phjlHZrxtt+?y=zH0kbt~=M3RtpYy z%M<@W++Z$a=m<-&U^g3CV#ftq?Au(vo+b7(S{n%5Z2N=ZG2$0r2fT5;E$aN6s_{p* z>LWnc;t=(xZXlX{MrHvj5W)QqOce&UkQa8a+5XWW-TqOl7D-NA{01#`&l8qj*gs70#Q;~( z9^e)FJ{iYFZu(bYocwM_ZVOT;p!`G`5QfYv1RBE(vKXQU!b?4|Mp25wi8kMlHi?k8 ziZBR~8n#0eX#e^iHST)})tV@8&|trgBg=W-4Rl>}qLZ13-hT?HM^|<#gzP#VEI||l zkrM1Kj!j=#k|=1ArB%C*;JQ3+O9tHT?30-KEt!r!(Z{KkK7)mE2>p7C50OITH-<ls0>D2{#72h`7iftqUqK6wX5!4M~71p0<5I*4pV&AGj5$a0shMpe-6&_yCpy{y+1XX-b%7ShKItuwYSqt(!vNIaR9;a2({ zT@6EZLGr{1zC41jFtGnKW-;&>i<}sNUPz+%#l>5etOA-qg;`{6B=e9|zB<%}4pBt( z{wq60)Bi81N=%J}XsGd^)RTZg!uhSf)n#I%toLzY+ zt^Ys0=e){tUKOKj*V%8h>pN&PJ5cMthk~m1 z4#F`a)p&CznHwpx-WvgZ&^0cNG<8Jj>nr!w`V#$7Sjnb9{8>f)?--8yhj99Thivjr zTl{fU_d(ezeU3-;t);te%AE&0;ZJjML7>T+5s{lC&Co=;*IL#tiy;n$iL?{(u(#fR z6<3q$38=N7f~VyGrDhrcMB-|qvjs-_Y8LagNXRx-l^rPopQl2OQOorwugsGiY=hr4 z9N>4nQmg4{8w>@K5L-swG?Axm0H^;?NdAoEClLo@8`#+rJ*m-3aEJP1pL6POV3!!} zD7#+z8+Zgd<#lJSAh>wwtv?032Jo?{Nk0-$)gMrumJAwbbgGJd_W#s}JVYt~T-1Jo zI}LapHv?7}p7rYETf@gU+X-%9Rq|LqnLa7`UV*JEj!;nv5w!&AUe(=^$Lk= z04fen0TjYCKyBmJ0&MdGR5cfyQKEh+qg{}XT}WeIP&m=lddhA`cgU&Z9_IgpoCcnZ z{u5#K6bZRXFCC!~?V?0l<4LeYGJ`6Kgu6Y7gxd{?gqq``Y~bm@<=EA$f2@|wUvylA z0Cm?Xo|COO&tJG!YrYo*XrBN*K0pftw8TTT`5v;j4fHT*>b2u5W+yguJQ51??kcd6 zEk&XMo(fRIetiT_1Gv;4ZXF09Gh^L&5FtK;fQQD%9d4?Pg&c3^C^uRI^A<8VH9a*v zvwofD(rN~dZ}@v94fpN*+&y7)Kfpw`?XZa4;(84TnpHBW?H9XdSlNuKuuOb|Wvpvn z5}D8ktFi)@JSL`AO-xP9o|@5ySHVM}q}rKiKCr?uFtC!)ut5N#9cM!5(gW#C`9h2HytlY&V zFffb@SoS%G^!Xr-AzW5!-V?;vyq6C|%j=AWDIE!1qlpvQ*6zs4Ro)3uHnRngp0%EB zVDlckk}-a=eE>fYwF_%GCb0qek3qF-fEkE3AB=$(eKsE?4f{0yU>|oFYKdXieuR1m zrZvEXEp>5=O;v@u{E)~(^DmKstyU-b-UkXg8&+_G=$tR3vw<^^4N`Dtx<0JE!|GBw zcO3zCN*Ojgx)226Ok?sD4t|juf}1- zNe#!Y2zEY*ONH+OBo)3JrHXd%0Vv$}8dST!f%F2DP7r*bK?7$Ie7}MD@3~Wvy!$TGBs?c);^8O$QW>J0G(e zb-^RfN{tq9TuvH;{S5Aj+=Upz5zE>EZH@;GdJIG48UexAa; zHwCIW4FJ%TZl9XnSOAFLgqqfFV8UIq^4Cl$If-w`YUMPQ_scX)85TA7K@gG|V4M!b zXmx+I_Fg8+0A|YgIYOP z5az{JQV*vutG6pmgf9vcL9`-F+&<>KHDLRE6W*ZFt%z(RdMB^7UjX7B!-)*}Xlfe! z$5ALbeFBi&<#Gdc`?U5+APDzU0JZbH!XPK7PXoN6Q%>&83pL-d#2J{6FdwrLiGy?3 ziqV<_CnmKCSXjYT1c5!j8bWg)9yVR#$l<&5ArH& z5N@Zgo;h{R8l!y#$);nJb)-DFQA1>sxfJ&;HlY%uXaQ+3S-~1i9(08Kayo() z=9iNTc^?P$U7`~FUIf1%!36gQD3!2&7(q`nC>MazaQ8J(s z!|RQfap4uFyt;Feg|-(0A2K-7{yRECM7{d*(JO3V?t$aJK^_ zDE`t;zT8{f&kUofa4+XtUAc>0Vad?Z|B>70gc_lc>|r48Si9(CfS3!v88Qe|{!|;^ zyc@XNGj^wyr-E8Lk*+*<#8onK-??$(I*0lP7g>l9SKu?ps;P0Q?;Hy$+ADQ5GtvGB z`$k6x4|XhY`+bf^=zna6Z^cFrv7gA^m;Jz==Evhu@9#_J3q8;p}~6N5eh ziQeGe#XxR=2cKqueNw|xz0AsZ!r8&fQHrK|bLzWg?Vxxg0 zt7R#~>t-ZMp^YpfhHZ$PQVdv#VtcUaf1)rO1kHh~QL39w^fEN$tFooH>U!OZqBLhJ zCT**hu#`0+dg*|7tZ3+4xkcC1w}Mn@+M9to0(1t6`fkW`GOc68noR3^7&yo$!1YJ5 zp3(ukc)dxB;K9)+AxiLv4xLEkH&*B-3qU%#p)_;kO(<14**o;^ryR3E{bE;it>xCF zcA0*ii>1d{L4Lx1>>43JOU(FO*{v&4lf*j3cqa-iP3t4TVW1;oL&Ld|kM6Z@bqK9vXHWKm(IZHRSNyl8G7taxJ_AzUb42IMh4FE z)5yR}6X&3k!@vh={dF=ZB~uUr*@_#C`VdHSE~&E{fs5E7hEwM(!VO0KNtPdYDeB@w zu)#CfZ*YmhI@{i4NQpk;$!&gOm1T+#?FaOE0iGe#{m!sL-MWbf)y}>s>GM#Z9CWhL zP?SURh7_yL0)9}>zLrTg4XbT&R#8xQz~&Subp#hQy|~%SAT6)}2rDYhW;7ik_K)C_2p$l@rvPlT8CMem4~nHvjo`rsy1<6e*kf0yxCsdlo)s1fagXNK z#NDf>iuRn2Df8e^gYN_EG5^AOMw4wfFD{lIQ2cAvOp1Kxa6NRCm z2|Srmy2GVq6AjZpanRSG9O^K(p-P_>!Dj=McOD)=b}$&krZsvS^$5;}-zBy#0j#rg_0wCF7k>y&jZLeCF;)y$mcj9=HbA{VsrtyU8grAKPh2 zA*P8>6*9oGhJ)pCcT&?vj2t`}o#vfMY?vqwD3a3A#HPSr5J60NPIk)yY34pQg2w@2 zt3UIhY29fhgLl9O2LFe(NZ2Q+58e@uet;s@gXKp&jad|`)udp*bg88c)bGN;T!VKW zYlv~Lt*&G?fmuh#@CF|M_B<@h(lf-2Pm9QPLR9AlV5B~R1}9qL)&OCUtjV^`#bVMh z4p$Zc5;9WM3}Qz$_+X@iLPy+Jb8J-{az#Xu__JXrLTK<+x!N~T$|Z$RaXu?7xs-PR zIHiBqPZwCbezN09&XH({^O++T0va4n7KyTY%uQq5;WzFwjK-zNYs=4ljh^iB2}8ad zL@4(9EB&$(19zVQGRO@D!jgKpP>0nr7}PFn7*u}=@(Kos@@~=jG6UVBldTl|s71|k zFE@mpb|QsW0DMGTEbfF|K<%>qKw{DoEyt)ss!!*Pw2fCYShD8Mw_!R+?YawDx3$`T9wg z70(JKvG?^>kwZiri2d}qK{Qwv?gZ|4dSWnG77m6stghWc980psLQ4k!Zb?Mk2_c_2 zl?m~9D~A>GLCd;ndnIpT-MVqup-jvkxa#P`E+M<+k7U1>x8v8KBi{4EOX|G{j2VVa zyMYoWQm%SLX%G^xuOJS=l@S~VC}Ubh&?1*j1BlE6cT;{>qZoot%$M(|xx7^r_|m4B zkewKj14Tqvx)ehdD?o{kYBsX$KzzWPxCqRm$nPvuyqdwIc_yI|;}ANhBSqmjfvB2n zum_yuqlL=jxY$C4d_bmO6IMSejz&ReqjfW3Qx2EoB6e6XKp1xD_}rrtXwi5;L~f-BY&`@O`hoFFR}Rz4qE` zuW1iwpK~Wxjtq~Fj;$QY++V(SeC+g*HIpM*@uDoxt<;iY>BLmFd}K5${`HL2BQMJO zeFYo!BP~|FYG}=x$*eH6;k7HLveSpxWX1C)CRQ3Y(emMSS+Qcx$mq(fRUFD91BSB# z;2@Hc$x*9Tn2-8? zr5PIjT3z%@k2fnHUO6^wR`rWFe~5TZM^V>HC~_K9(wM|Vx1|61=?78Ldy=o`)>QP14Hv2wG>(C5jbN;@=@z+zxU!P$ z(i}C2Ls8nQipAr?J(gG?Fg`IgG&Vl9W+KvQ6^l`w?TchSxqLoAIr!lKSry{tVOFAO zHN13k?V9CXqz(W+0`p?Bmd!_20zVRBK)Ip-P6jC1odR&)9Cq_!z?tTW#}a071ebhh2$Hu&L?EsCX1U_G^E7q}Q^>LosnHe1iucD;tz z%E>5J&6O9TUM~MGfQmyG0o-#Rq(4KF@a3JM6Umcx3bhmMKQ;-`>YYZ(kHVt$c-PGC zq?agg8G6QqYI=*EMY;;Kv4(6=ZB;DX0vf8J0N#zfhW;La8v1(yYUq~$l$hQJ@Buda zcYqH@fsm|NVf`l5Z&A0fratD8P%gv?a=6%vgE866)ma1o38wr!G=oi#60m8t6Woi# zGm%JI9q3w}GTeL!4LI1IvS8uZY#>QYWb6INOCleL;0FONBEn^;ZxZ}4N;Rclj?zkI z{FcBU<&p}gSb-+_E{R6SKxFWiXft9E4T7vLwM@6H7W9;r1Y#y3FE9~}2BtcoNLc}R zFtW0ltZ-ynWDu0{KL%Wh<>L{&5}*v_699$#NrUpe*!WW@rJ>}U8@gn%4wc?a2u5Xa z>>Ijek#i;qvbe&UbjzZrC=#==26;2F771r_w@c-_fE5Y}&gO$63b!GVtwgD9Bhz7E z`K}!JXMieseKvxh11K}X9OBG~(~HdL3qaUR3Yc&51q8nY@EOtFk}koG>yl2lO^g** zT#+&IOlg*~PKYhbxglhoMv6j?!C}GBQY_YyjK=RnF=o;}%mkVXa8_bl(jgsZkO8jx zzG$Hy6tgeJQM8bsgMj~CVyDIf82EOir)Crmrr`XA9QHXN#;QmM1hfV4 z2Qrb$JkM2JL5!ScXKvm^daUY?LT~c^8_=7k?5{@fMu10!nQc~WyiwX5Zwc(Mbi3X% zHlx=z$7ga@Tu#*M>wDu(Z&0nZ%!e@>V*ttdjgJ7D@6p>)G-^N;pX}~th4>=2Z zUPUf{XrPnxk0SWv2>!%C$M8=9zQ!y`QraAaFA1O#i3a}v+e$qD#``0a^lQ-FI0@3( zWevBX7lF4&@D2mX+5(grzk$iwC`jz27B_-HU>)UIotoIeVK00ie}hQ00@(^s@%1i% zTDbfYpys1r0UVUf*e<9ddq6u5#`zg7_D*Y_FlZ;z>FgqvgsmjjUg$5|)Bfd~D8yeQ zFAnbkC=P!EP#oS1aL=gK2P~U!Vty1=Frb`4oi$vl1^L}=m7YC2eB(B}YqP7l4UVK; z$1xyD#t=xHiQR`nY4`pJ{tgIN1f9-`EOvkt1sS;ctrdIscFfEWgFqm^0?AS`^B@Yu z!9x-JJrKZwMo}rw+ysOf6$T+W9&7@dd>GpT`YI>FWJs})gC&z%*8B;*OQC-TD24t7 zpcIPfG{45U)*-=Ni7!y0arz|bAiY0=n43V&ZH;>$bq)pb-ut;_tilRKy**%%TdQzL zu`@0IS(tbu2lh9TC-`@O98ylo98yl0!_Tp#kn`oVpqutV0sL4C2aZWg7aFaW|Lm6Q z3^bDR%4p+}AvO;);r}(3Z83VwK8-|7F{IIN@|{=} zofMD@!J`1lKl@`1yFb%SdHH}LXz4a`nxaU$`cb!6feMer^G5+xw_ML(rNg1Kt(Q zcy1AvmNXR(2cpVfi01PKis7~EvV1l&`}M+@W1~f7QRvCiwb?$%(jh>H3sDi{QtwO* zBM%x;jWi;@Ux!8o+^on&ave&9$Te|T%O(c^WcejPoU=WaiQ(6~#iP1e%~cB`(&u#m zGx})(n=hdEVrOynTGXjYIlO$iJ?lmRclP-n^@3SglY(#j;~Y9n>{cRD$r#1QB9Q|= z0bq}Fxnj?KN_)17^&|gUp*001zUI`%Cza9%7@N}GjY_c>NF7TxJrN*;TI^L?n(v{3 z&7yV-aTU9S;H02=wJs^rIWu?3@z=XVVFBvJlP$@niTCkAn%iHFa3se>Hm?D-J?TMv z15~(EA1r+eN-OF&e>~vKKZ?wsWEneUtSS0Q2`4^UZ6`7>2Fc>-NV$H?$)VVwB&77j z)911QeP%cg1Z!fqej{UUMp1M}U5GDe<0sW%e|k#lED%d0`zzF#Vqlz7c-fa#wf^-S zucC$)pfOs-K4Ahewr~ewJo`14pzoatv^#j_@ z(yllfq%>DN1E82cFoMrCusGWIaZ9_NOafi}_^=IWJ67y6!1RZ=q89dz8CK-fkX`Zs zwS`DHSPA*r$cwq>MDV!)HNpO~K(i5l8o<`;1HYn1E^qN%LW>EPcq%`G_O&P{S0q6d zh_yq|vsj}?349(%k8|geLoaR}4zq{`h?PdI|LrMj9E~;H=L1wvhez-T1B-D8us9B- zmHL-p={Mc|9|lZ$fIWe8mlA@z1syE|Ew{<1c1TcuNWFE59BW+KQqC~lfxL3MuJ}EQ z#8^t}Q|Sw=v{=tlY<-He31SraUU5JjH;HG7Ufsz69EFpgj{UfFllQ#UYE-y6_|-O) zO(CHsLl`;|C2nnRcc<2-PvUG`!MHf{X_-VuPXZ~81d~_sE*{?HAm?0zl2^#i4pFgj zqs;(F*gWd9^C{$uQAi>CM@adJRw8xb$=S%d86Id`q{81KV|XdGnJ=Xqgf&y@SuX{u zIDc6LUk-2)hxQ7C@}-Dj#l^kI)SnV|&=jI6J}?_8SKd(EFy&obE>ftv9LYy&L_?e_ zK5C7Yrj0b6TO(~@7#oSM1?(tlT1Z&PYDje{D~gXuthMfFD4W4kvKC}}s`sfFL&hgV zIgN(+L1Dv=bbUR{+t z?>N`TdBn8aHNp88_pl}o1a6ud(lX>_NXsKQ0#JqoQRPdyc-FGdwFZU+>f*JC>2ZVYf8{8^`uy zgOB0!RiGv|#sMB%V*?9(7Xe7*93auPyd(jCJ5;jy3Ynoiq8TSeXQiJI#>2Fo(wQoS)NW za$FJ_-364T%2xvvqw4_bLMm00WxKEm_W<3UosLG_HqyH5w+fDlT~X3Z)Zc5+3GbQ| zzpH6hsIkiyP`T5?1=wUrVVcloJbFq4$m-%ufHcJXEI`C6aEzzt_CCMfUp z$C&vwaX1fvid6i1fRfyLfF(qfpAArph&LdAjn=3zBwMN@2^zx=*H4DHw`d2yVOv<& zoquql|+Spcw@dSpQdhNXXGP@t(?0fe4>hZ z&^rJzROd3J{|t6Q!FCKx6$Hwf)QO2uTK*qW+JqYS?A4(BV6rE<0XLnQRE0wNe`2q( z|0l%$li_(wKG)jDWwtXkF3hl~b~9}>jTZX4ncaeA*DdJg??GM@%6kdM2?e3MJkm$y zn<>?cffMC-1+sCOsmpoSps<5PItf#u&Y|(#+tmQ_3-I#D*g+U^u^uR~15scHq|IJX z&0#s;Vh5^0YaT$^X2iQvT}Sn zQ2gbUlZ3A~t4fQl^365A*f4Y|zP4z!@bGEtF^ri7+lfy+6n=nZwc@rJ1&&)B?$Hk>$03 zez!AN+67yw-|IlIKG+Xgnfl~~*771CsilVcB@_f>oEly`mAtPY`2qoF8g3zYJwUhC z1bEzRO9~3nODtW+$Q9$1QHzDvwtNNqp~cfIE=8Ju)e<*t+!(>H5uAr1}v=LI&L;DwwV7kivq zei*?Y5eynCw_3iu%a3Ji6l@0-cgC?HuhkM|suiO~6C2gFp+=x|Pf$_X()W8;AmM65 z-mMC|`6%xMGl_zG^_wEmG=jj&2fXNK4$09Fz>1p}Zv~hb!e3S84B@YlNy^1FbW=m! z5L62SXQtfro|wo@Y@u2Db~LU{5RImlmEudY;WvTB=gPKYqFd2?HATP^wzD{hLf}lS z9sSQiFAAZtGxGkVrm=I-v%F4Ixc3HkP802wf)b9G0{Q7ZPm&*Dt5Zw!y8zb309`xI z&{>0%idsqtcUY-O%6D3S9giGpg%pKwESg9NzXF&DVQ=Jv5cY-;vU8Ad0h~mk`6!g- z#(1T|?F&gbp5I3}Bj1%sJc4ux+0t*omSXt55&SJdh^^$BhEjw)8ZBDV4^W>5==zlS z&3eHP>IL7c7u-=V*jg{RtzPicdciO21@}O1W4uJ#V-4m{VHoo1WmWwq{-Iho2O;mLm&QS}nMH!mwEP06#b)1IZ;wHXeUTiC zzVbf<)az^EoGUxFi^MdJ(c}yylE*fHQ69d^1vnyh%VUctKYdf=g+ZB980zEi>;pE+ zv&hB?-YbYWZS8koUDFTN3;t9u_)ERuZ=TEa9rkb}qDTO)77^sa%{eT%BwzHLq5-T# zK8q~dc(EVAqJ4mVF>vU38zVVvVRZFg>u&66rRZd<$wupexx}iwp4ZbkSw(Kp9C+;8 z(Sgxv-AFtVOKx0sW~0G=NY(>YXIt?126xM>FF5uNkQg{|4$F6MdM|c?mtPU($5HYz ze=&eM32iWfJFx-8lpn^@kceGm$)Z0T=3_noj7F~^*H5cYK%?xGR`EOnde~2%Mo}Qb zT#tK;v{Ow=Pfun!T0UdveI}hs7CehR1!i0DDS?KvtK}P0EZq&@>6(F0G}wBoijxSq zD;B=HEs{J_9X61_V}ZMcq2jFuHO@jFkB;$w<1CJVya8J~Kti+J+P>Hs#r}e*WaFP5 z9f~G+P3Qp)@bJCy z1wb|_z8e4YEbah8Q&eSgCxAXg1BfxLah(Q2*^x=H&f#pKIvCOQJR}(qXFM>*gUiNQ zAixmaxX#R6pXq2^M*)1E#MyiDAfE&%40aot(+MjX*ycy8qyN~wUbtfSiV|YSdLAFq zZB9x(64e3eHO6G)J4kNghMQic%O{O*TXDwA`Q^8w-nzNWwEzL8zgt~k4cNXQkjG=dz?Deuq=czL zNtpAbBz%}5=u$Y3r+ouA2VE)S;-)I=0F{Cy$B-sU8g~i_jGEUXNs#Pzu?4k$R|zIb6p1_Ti#LuujD`?SYFUK+0Lq(Ev607XT#l zK5k<;`3q-Ts^#6wJkv*^LJ#*tpY_FuSshw7A7u$X>=M@?@q94KL$-W8aK#P6a#K;C zYY0iZ1%x4jLT8r65>d-tuEO&T?g*)km>zy70mbA+^3Y z4om#K1pSHYmjaXlz09D-dn2nDYvbe5OV~Esga#A?xP$n`E0(c>HlV_}El0*C^f5MJ znSVW@c(Eb7STz<@W0$`>_@G5Fhv!+wnFM;Z)sWs5Z9XbhJ-$jKEKcCkq$coF*bH44 zr&`iHkl+%4&my?gKt;F)o&z)&R(2s0g5x5#xp1JEJRr+e5M?svjd~22l89k00Eg>P zl<$hv&Kg_}1d4|IjAU|hLb2ut0yoO2G)m9NoD2DJA_g_S>7JoCj|eR`&qc+x2&Tm= zEy)i?S8h_`2w!FSCf$c!Fcf(8HE~~8>a&*&CJ(fc7KRRLnchVP30{e8-0KbUWGm^O zX4de#O+jlkzouPkSdGSA4`4@85N8(T*aJ7&!k2-bW;M>O)&Q$T+2vGMlUhXtSc$6U zDUt!;?nMdh)zP2kWvm1d(zk0(rM1^>SQiANzB}kVLk~+@)~Jbvwt1Q*#cKgdGBi^;^jRq7blHSpd;>2RzJl0X0VE8-MfETW z6k#La#&5aeWUu4bSk47bJCNc2F*)rE`|j{usZ}foIbQu88ph3*#Y67%L)uC`nzcwM zCo_)4LrXD%EFM~hQZmJs)0Ic&9zI?3VssKse2b4FXwT7bB+;iDhmXV1L znIG)iZb37w3-evbns7npttkqFLi6A1D2At+x7BOX-V{-4FU;t6Gf#08($g1aT1L0P zMz)EiNAnow-|qAE`&Z4k!asBwjk0iWncQckHaG;EctFv78%pOu*v*RpZUO7bJzAh= z+n}-;_#y%JGlzWr8yg_0=%-;L*nC@e*KWv$*u1FLDaj>oHck^p=tL5^wAK@=H$d^@ z)O_=NbP)HfQJajq)cQ1qV+i25`3WTN>1LjVCb!b+^1oPOW?LJCNN-1S??fwNZKLFv z2SIoJD@yJY-JNRz&Bp3k#Fya34z?tm&<7(^%Ik4B(bi(9?v zMu3*@@Xi75rIL3Ul#L<#vF+&r2$1h|f3rd-{_W{btkIcL^@1!$(!3GL^)<~v-+C0$ zdpMV)(U*~2f#mAhNIz)_O}61e3YhHk+ir={VGbFw{bzK4#5oA01pB7Bf2GK8@ruMEd3z; zpQ;HF%#oSq=TQCmZapRg_;Ytd)odrQ{u1OqgXGtiWd6G&)W`Io6E;N8`0)r{89~m6KZ2MocG;gT<4XIlI2##-B3dqk0rsIN zZk~@+YkMC$KWZgm6n3NSkuPUKc)eS)5{7MLa82GTESGR_pGKhucU1%-R#*Dj2vUJs zqT<0&lit?%7=S+q7Du)o5Ju+K(pq2CpSuLtQUu+AM&a}clgPBOKjK-#J;+*b#F{@! zH2YI4=z9_e|3w4cFuxSRYa;lc5xmyGzWv$kIscIV_78+W(e;$&Yp z2qLL7PznZdlVzq0^$|G)nEJ7E0{kblgdCbbv83-ffW$qt#UX;)vp(Tcmr=1 zNQeB!TyOOChM8^j=sLCFBctrH=-o6tJw*fWnj6=HOI>zUy=60KBrB0XdR-?s4B_jo zM$O@P+q>5Q4+b3@w57!_Eh*zupKQJ5$u}j#!0sm(?lsOqJ@5DHK31K@I(Nk9c1BlA z>-hdjFyiNoudR#W4c2qt1?2j7;6j@Hp9nqx1Rity=e}0J8;pGy=n3zgKz8SBfP&rK zZy9%H3ai`BC6-`x?!_L4>BQ(B0$s88dxBj?mob3Pvx>f}ydpl|)96TdBPi634g|By z?4P@>Ow9F`r{2mJ0>Xsst)Nccs{1(a!jQWx(`w3P!91NgQtdRd4k%NB(<~7@(PmvE zV9I9wD6gX8{$Sl}C zTfRpus(D?eA8c*qWUc@TV>O*-2cq zQxjOk+UG|=i;AXH8Q;nV3dK&7AT=GfEJ>^4aMT}b|N3sNBL#zQycqSjqduPbWQ#0k zcc4(X2}ybe7nDJy4!ds*>f*qJ;qEQ7gUIgPF*x7*uK)Y>&&7)R=4oggtrzT8FW9|aQ2zj3`ItJ!<3g~r-z*AZ2*=`51$54HlJwH6 z<_Zj^d=lz4=j}}p4z6%Q4Z^jm=UY;KGAs@lKHOsg(T{4U$Lk3d9gG1&zjG1u6*~zN zYsH`d%<8CmO;7qXNS=!%L5#Xd-6099K?=oNx9SB}x2h|IZO>T!w zpShzLNR@2XCh_VR#iqxASXTe2wq(GOY(jn71@h~W)R@gSqM!Kau{sJ!8!^u6Wdys& zA*bZMp6M%)ID++PnkbI>TG!Q4-CfIZP*xpi*5bBRoXX=(@!g`WRvD(wEGjN|>gG?j9-dYykr8SkJYA_)b@wM#67!%W&g@`8 zRXxwRtd7P|H6BG4dZIuY$Me`1_WbfREo@6N(_=Tu-$Qe&D0ipCb{xy?H^kPAEwvAk z;fU~1BW7L@?%=eF?`~jGI|&2+a#4H zize4tVRb30I{uOtKd`R%D%1wGlm-@c$be7BL*x_eRC?r3Q3Uq5`#k{dGHoM250Iow zKzObt;ay5$gC#zr7LLE2SkATLuA4z!TEv;8v{*c1EiOTiQL7a_na)ryL{(8)QZ520 z+3+(OC6M_ zw1hI#rc`BI)m7#69j%tls4r-ks;Z<5s%i`bITzs04^`zfNv7E|as2sB`7CSDr7D~! zMUM-rGKX`1W^c26_dN8IwH4pJl}jyD1KE_bEezFYf{Kb?n=hY_yqxWDfV{L>9sw}X z*DaQd&a* zrZ_o76{a80{mFQM{D*{Ley40Q=RF8EJ zrTPodsmkD{SRi#-PFF;II9?iuWru$<@)$>*lMn|{qj9Ar)qPM{d5R^@NKOSPKOF)X zjij}^Wm|hVp|*BUgz9^X$Mw#oVsBfm@l1kkJx(#2OEd;BaFvazHPfEJD2a7xT7RP2-!?*!8gC=Kzyh1G%nO&1$qB)puJ*Atl zCQK3bLfba+#Uqp-qIfR@gcQ{OgUC3!)-AXn-kuggrJcNMwU5ImakK+PJq2#YU6P3DdO` zkmH-Q6bwb=;$i5qbyBTI^w78;G*TltQ61Klpr`4v8>a+}G;T+y_3hPj8v1bWg5r=* zEBiENaURM}p}68V;G55k@-xv%RS7E3v5JVQr7Cpkgc=*I76stP76RN|>zPY{hOD*K?f{Hvql1ak7G5I%3&E zbh-pdTyIwQA+K$~+W=}bZwIJt0Oi?cfDNZnEudC#ffjE$#*+)xAWT;GbNODvhBemK zzoGayURz{BANW{86n;FYJRYzn4#@_*3k~_|KJOf$)-|z@*$vo7w*KxVDt}720p#t$ z*s%RC?NxuI(%*#wiRmJMQu-!w`$H?2>ukT~_A8wPcQI!08BQC|T{{M+pidP7$jy3Q|Ps>O2f0sre9S@{0uIoxT(e;X)wuT{!2!_LJuR{joGw z;^4*91wRgM*?hDWRhsPo9o14ScOX*i`>n9`Rg8~sgBh-ZSZl*vlwE5H7v&strXM)g zXYI6B@1BpQg(7gGx6`&THWWvJpqn-Tb-ca5&ocfw*-H2QcE(T~>4dQzhBmc1nn4c( z&00t{AX(B~SpCGx++Og*sFxgQSCYd=P^#JbqXxBp2p#EI$F+6u7{!nuf5lD_UHd`M z3GWzLmwo|8ozvTZr`1%nfoT-HSYR7|j$FNF;*|%4Pg`^gr+FZJxt&giOYk6|jrLbr zqL{M*<{{a{8rZa!eH9=+>DSZ9&3!paX6Zl0(f>e+%cIxULs4y8)MrQk=`4}X#hC^nI1BU2Cqd8_67&*CX~7Iq zf-ONx)PoK5HIAj_|HlDkauXN=z`cR7#yb6quCwpQMDvuanZ%5&VLIZT4G! z382J?;10;f!K4+OAr4`!~lZ?sGTX(yM zNv&V|^}%ljt(=tG{O!<^AwmQBvQ;^IxQ?wMsq!lTWe?W_boK!7Axqq3NTDM9wjN>+ zI~myC8G$L=o$(AKYC-R{Vg08SaahYoMzdn|@L1Pr2_r`s4?bSK)bQPGau50YD)Jh@ zjRv^^d<~`2<<|i&X|e!GY5!XHcn`h7au&Go+vTHc$MwS#(|vOk4V%xzFFxB}g&*n- zy9^zvGJ+*BBq+JM15M;AzSIA*lAz0xDO@O+vCl{dCRP0w)c7z{XJH!o_pH#3{QCf( z$q!$Y=*RbMfN$KjJ)&1`0G_{dT7JheCX>^L*JQ=W>aJe{UkpUNDtiI|#;44G9i{|> zCd!p#!;@L@ozG=@rm{IJ3p-YTgpJsc{hy4sPR}oJtOt4d5?T+xSkyieUDC0rhR`oU zyno{yUD)%EqziFsGph)i4b4EAn}F6g&kk>%&Hb`$Qm%m17HQ<#xWWVP$oaHEd8C{q*BALjrAn{Zc5*5nA0Doy2 zh4irA8Cq^GmJTqu_hJ;gQ9|KbbWryM-6H5d^dRoBzIPV?I|JMNZ6GQSi=cHtOr<0P z_n&lUZjSdxxRg^xWVIKkn17s30+agv((?D{Pn`WBf`2ry$*lxA!_U)B<1E-lb6?L8 z;%cD}D7cLlewen~5rb8ep$5O5pz{=G7F;~@vjtuD2j&zPd59*KaVF+$`mY8}|GI(| zw$BApI8?ALw*QX8T-1)DmiJ)WZz70)|k@kfg`Z3n3y(vn;oJ3Nv zxy&)lN@^>S0w!`9Hotu7r0^(EyKs)Be38G6nZNxXE)tqdI07)5+JMyWkqq1QJJ+zd zRjKaqOx@v`(m^|8zL*Ll;F4FOu@F4^YV-vHvdZ=sz#R3GALJ|{KZuRD05d3CKi=oR z71kKEItZ7m5&L9}S=OPzhwCpR;CJ0|F+!1bXc9cjmCfipf~9+*A)T(lNSe%M;G=Dy zu3tmiIxe(FYYK&^Y+UDa>tp!m5I{Q2y^Y6Nruzrm%VNw{R8uQP#%!kZsOAv~ z^~7v%HK0v@iVKJKtYb{L5&(EHMP;*Ngfvh^=BXg3uymr-_m|`#@_ux ziK&(exg+8o5k#9dmr;DVRpTN)aN2huA>D;sOXd$+ftA#l_yt-t_Cwt~)c+jN9Q$?F zG5^{*3iR`+?Nb2~4N&pqs#zR{q7n(e9T4x4wSNvan%JPWPX*ZM2lz7#x{p&n6?K~q zs(xvuPS&>q@?TVGzyjP-$X_S@hkOoPCq5_dT7W|N+%o{G^gw{gH9hdz&(A2Q%D2L{ zEzPY_lxT0v8T^TIyxsfHOF$38@86AP5&Wf}JHfiY^s}qoV%Jb(|Kqy-rGGclvt&p9 z(yz%s_>XG|@-=^P9a}}4yIEBSPw9UwY9N<3pNc#8Kpsm)S52RIrsZ{AES@s=KPLEu z+yQphJ{6AD#;UdM5B=I8!!?NCzlQ0Ac>$~G1+%Lr8trdMY5&CcAJIqq0VJo&{cb~D`_yjp@81m?>nE3V2O7U$ z<~0tm%3%D%ygYv>$n=^~6V;QqINd+K-$yo>sdC-8i6L@NBm@@m~QB=CYJM*#c~t2i6g=!vZb! zZ6;sK5?j=sPGF1e4u+NzzxV{;b!%-&=ikJQzbvNDR%mI6`ZG=^ntdi`Ht29}aj)fY z2Y^Ch2b=AGd5~`Z%dI+o2}7UUrS4gy&l|`JAo#{1mbe(s!OD=iju&_s5O@^PfGX^% zq9u*P0rK%c;|PFTSbC&E#U}_ZHn9Jt1dj%IGVS4F1NGT8T`WHsRYMpjze|!IZ04g^ zmGgsTKp1j=9NkJ}F+>eyTX&5D6onIQz8`H8A#WC85F)iz22r5><2`EBkG`k!gxID> zzm6lr@x0H3PG%x{|7!FbUD>G+vg^863{eckjrfq~s9`b4z82NI#lRq&D(-kx zVLVAcOM-mF@Y}3fCoug1y|?1f+rv~GX9%gs8ug!B(^2iyWyxUP;b#FvmkLjJ?9T;u zEX%ns^;=sD=}QgG=F23uFQ(OK#%!UIQy$F?Zl%xcH84~+@t+XE6C-$%f&HH_iy1~) z`g_OpzPN77l2rivt4-6~p=<{o>c~1sz-a$fK|NgX^?wF6JQSi|X%#5+Zi|q!BzI4e zMFd}eN<_jw#V5d|1|o82>p&KJ;G&%&=EE&NBXV$qophDjpu}KvmYN-{x1z zc)jJ^Z1p05n!{ckL2MLU=}Qfwdi-1UU`#KP>1zUr_Y#)GifmmK$qI^^qt(u=if@1h z4;Sbu+ffAxJv>zi6_n9&|J60Af1}$Rq#ABFwW6XDp|t*Mz32R^<-96}SFg5r=4QA- z!i7TDdV18FW_i;q#MVXfFCNgkhr_dhlSod>85CAX%4kr*5p*SqcP$zx14;YNQzD4n zgwrfGP&yrNEJ3N(EVK|s)Qee)WWD|CzugjkJZqT&h7PZgyKNz>iF+z60}D2xi?_0U z4g#DvHlk)M4kF9}t|lRGi2c9vZTj!7*YxZigkwZ%Y(%3N)urB^Gr9XtZCn~Dq(|xN zqyF{!67*qN?tT2A)Nkuh)G3qBa*yQuJ7d5>2o}yZ%rHbM)PGSzu_Kl zF{o1bQSO?diF7wwZj6{HOr)KNhrRXotGJqsAHr;0ZHE;Uuz133)CO9HW-&|22f^Ob>b31}|O?Xj{pUBtkuHgP}kYVoQ)q22XbaPXGTP zc>u}xBM!zk(6U5F##(*uP=D-mM*R)&Eh< z1JfJI!Ft(ee>i@Bg`xPTqV~JvX~65c7a+CvIEwfCK2Ed>bjkFoARCn*0^77WLir~| z)Y7B5bHj3L zp!Jl!6yGJMu3MP@4{{nH6Ui*lQzYany>f(+&@MQwHC~0hM8f5`M8e&kM8fTcL^1(f zhW&y40aCo`)jumr<}W&K2|RY!EuL3eah@N)TI-Rc1N4Ld?H!=G0h;fj#^XGcwcMki z@mG#4n;JX4>w!?1cd6}c5tz{cx%tzuCs8U8PyDh)_Gn8-CU$JGZUKriK7l~ol*Phg z+*BJ2Io|G3VpCz>!e>?E6XQdZYu9)#t!Cf_m49|sxhr_Nd%os=b&71;(-s|`RQ{P; zhe2(>*flM9gOQBO#C7VLS476fVU5NLu6T@%kB*IxO`Rb>AH@m;N@~0g7y~Ce1_pE~ zd?63c8yJVx`NS?~u?hOFEG>5e%d-j22FCTYs=49!kFL9x?fw zcZ_&vdF1$X?G0As;u07b!u2cr%tQKgkj4YHO#1M(k(8XpH{AllLkPYkrMn${mk!@l@G z*vB1)T0$m`FQXoUX*ZeB^K~lCrm7mSx_tl0LhGT(09}>xy%!W3me{d4wFuGqornPg zlrG4+FaanW7Qfjtshp=B0d`9n&tQk=faPLilYEA0s<(bP2d z%TXvfeZ(N=E*~{ecaa-c071AP1E`%R0-cl7l>ooiEhl&8g_{4e#2J`hIDObkBo5A9 z%Z4YXf=wB~_+tIL(PNN#)3^Pkcwq0y^SvKg2%o?Po8fdOrD9!@z znU?S2DnoERte9N8bi2Hn4Kw1wm`||oaa`d3c-c|wHk0m^@?EDx-ZU+CeNe`J_C!QL_uUfm7V|0I7t=4H5h*3+XL4M(}F@2l+vz2KY$k z4JWe757Vy*OZJDE#=TX%duYbN1wZ(TmB(>S*-!Vxi>>Lv4nzBB0ckK<#u`i>bcB2p z9l;9oP2@sy=AdpSD#33=kX|8Kd<&&A?Qci$I}!Y@fjM8PZ+ws7JWB^21Onqx>P)?b zLNrQ->Ijm!$w;{H3R7OuJ;_4bbJ2^`?TwfuASc!h?$#g?l;IirP)=8cT+b{&&C$H9{fT!$91ycG1ZIF}Ka}lnnwk zKL}jxWy!!+&)DsjO9i!hEM0l-h^u7ezH{Tmb&fF)KG{NqxB{Pir=q&lcm5j`K`PYI z>C|DeXwhRd#}&YV5fYKzxO@jn0|%*^3V2r#Ctr_0pI8e!?l%_A67EnAnZ8l zwyZxV_U^*L`Br0}+5kU)w?yHiNr>Ll%mMR#pJow3*!sX$G;3l7I;hXo{1pi3%aPTx z6ykL=5~a{VmJ!1?L{2FN$W*r2QIdX_F&pGM=S#qD%|=QuLqonOTOR18`8O0nf0X8A z&7^JB!cdAC*M#V$1KzQsk#Cv!Qr`+vrD<;f>Jp$cNHkf<$+U@uj3(3O&IS&?lp=Yw zfx1WC+y$V$+@wYD;LG=gz*u9W zesqkb2O9PKp#9i2RltQK6D}#;x)Mx~9dRNioG7$3)l(7X%mrEO`Q3WzTtAHr z9Gmz7^%({}@Ha5i=&|Gd&nFK+fSXep}z2+JU+G@H?Mgpgy) zHuyRUm$FcVLYT18+P|in5~MIyis{_xWZww>Qv~;m;L{CsfeoRt$F5KT4iX+bH!KvA zofr+t?tHsNqIcco~mY}zOHB5 zbob^I4ABNINAKrBtntb0;N|3>=7n(&o@WV#-o4sx!aiFF(fC7{o;qVSzA_3!K@)f~ zqjZ-`%O)z*KXK64;JMW9v)G2;2S<3O6^Dt3`;_hxiS35BcemjMF+L0&xRqc?FdQd0jtuK07k3T@*kI`)0C`z1 z=X{Gn42mypez3D~W77bU4LtvgWuyW!+`T$awQv}kK^=>SsRypXb-xRs;%;(E%!h^= zlFSj!$)^hC7bqlGJnl|vI&jUwSE8Phj!A5oC=GZe=SebZwp61KoRS~@*|$cEDH5%Qm`NJ)Y1m(cVS?r z!K*rwiISxdX-4cSP8oyu8QE+W=Fs#EG2_!Ba-9&>xd9kSq6q~a)v3vR+e|Db4eNYD zPBK!|3_ghD_mK_?9dTbxG1hU&FA+uJ0mGKOW#4>JuJIL=a!Dantg(f~@ERQ8P%HM& z`so6z*RJe(l0$=Xt3|^dd}*>sl+|NyTFM=Mb%$Y8mm;q%Kle46K4XMsV7}{IODXo| z5q?>Tfx8a?8RUi%jEW0&{Yor2Z)}A1NlvouW0B{N#5RvJ&@DP~J;yCNPcYC;cqbaP zQy(du1klbe@vF74_nq37G&b&M>EMVZT8>eNG_x&%qvjD-yHg7|pd^MnfNEAa4KapK z(w*fNrGfGwors6^P}Lj`9dVeAUVns@vKl1 zdmp!o{18-QAohFfmeOEZxYJ&i-RX(JU|BdA+OWED6LBobDzGy6CrcvYPFRx>r#2zJ zz{+8Te9*FH!d}Q5TeD^ab|@3GvvnW5?OcJUqEs{K5J8JvHVq&s4{W9Uv@b)Q3;~6FL(SzaTi7!w z?R%V^7?A@+L^r?`Lt{)ULC$Ps@d5a-H*sO8qR4MzQoNeMqj|<-$kaT+kfLy$KrrI0 zLpIn0&hb&C@;ENGP$3_XQP_UZLmJU2I5pF{nXoC{g5x5Q5PM!>ZSBzU@bTqGjIA8W F{ufjn1o{8~ diff --git a/src/builtin/obj/num.olean b/src/builtin/obj/num.olean index 3038a7c20ff89e10c3fc7f0b33f919b8096f568f..d774427e4d3b1f6bb24c927b52f3b2fcea966c07 100644 GIT binary patch delta 736 zcmYjPUr19?7{7mZ@6{Q(+6bp&4_1^fPAr&CH;Dqt%5*Rgg7t^p9A()b-}#-hZY%4y^6-5( z*19*#@N4hccJ+-TnZK`-hw??$Fq#^db6n z8J_j{;9JkwMtl_y_s*&Cu|EL2f}%b_O(*a|u-^@VuoJQs4c^5ZSRL`n@OyLsQpra6 z9I1z+;YmfR;*;TVGIXUq&^+bh^&#w-`Ytm#H~15+3^L2@ zTA~b>DukgyIq7ooDcT9*5I6B|a!~-CN_nBxYQx*9c?ygXs=S7U^n%C-r;q&`tUUcx z5S^YW@ELTgWs_7T&=(vOx~?`sz%uy+kF6PAbYylLXSX-lZHUh<^P-VVGZT*YWiz7h zPv#!$bNlKh33Dr3Itd_=kn*P;WXa@HMv!kO%f{N3qQV)AIU$V;@8nig0)x5y7CMBH z#ihJY{ZHKhKbrx23I}=bwZeXi=pXP^;i3>AQtahLA-GjsfafI-94K98|4w>4b@$mO th2U%H1}B1Yo{H<+(0kLV@GDp@Y0y{kD(v<~D{p0vFbG1_5YEG@{1>Gy;RXNz delta 664 zcmYLGPiT^182`R+d%tfjSPm_;4KItJU2>>X6Wv%0qCYGh2|=NkxkVJtk|8?XtPD+U z@?#XN!wwa+I*gtmI_waOpdjcR!BE!0PAg~-c*yttn!7#E?|FZJ-sfqqDa|!yy>7>< zol)K1BO~Hq*l}D(#A&5F&Q%3lE`|ZO7gl#Sc7ulyce{w(s>~!wQnvBVV?)ft(C}QQ z^QV?OINTXQ&F95;pU$xPT{P?W88KTmVLjbR?*ld&6G4Vw!BGrP=4fN`kAjmShS#A% zs)c5l`mrS=X*6-g+@X%>^^I^?-IKu9R6mZVO)y1ss7CKm-}D)cTT2?`m=TS_LG=Ug z&Qa-RLS&UjT9acm7~7TGD)zXpG83O}WA%7N)P@+ti@QBtk~YAF&eGFc&vYiATuoRM zZ4-gGnU)iegn|6KWnjYS+&C5IR^(PJ6Zlh4@*-7|8+)z{;Z&jR&`kAlouNfDyy<9* zW5%0ws?9w;e?-;oac%zV|BMV5G8Q-%4`U&tQ~qXN^3Tf+@%gveUVO=#>1Vc}h@BWj zu=_a!J;~L?g|r3naw*?S&+|3`wKwO*iQ+itsXqiSR~(~H#oPN!v>;S+VyUzu#Q9o{ y@RyUk>v|=+&*gsXlpk>9fK?!sN}enayY)Q!jfSg7=~DIEzOE5t2+(6}%l`magyP5m diff --git a/src/builtin/obj/optional.olean b/src/builtin/obj/optional.olean index 12b7fcfd863d81edca584b849025512e8fb52ca5..d559e0fe1ae86ec17988c17a38831452b3d50457 100644 GIT binary patch delta 31 hcmca&a>Zmr5IY+q0}v=~j$m(Rgs>$xKjp|51OR?p2O9tY delta 31 hcmca&a>Zmr5IdV90}wE7j$m(RWRrlfpK|020swz*2O9tY diff --git a/src/builtin/optional.lean b/src/builtin/optional.lean index 2b37bad164..a61713dfad 100644 --- a/src/builtin/optional.lean +++ b/src/builtin/optional.lean @@ -36,14 +36,14 @@ theorem injectivity {A : (Type U)} {a a' : A} : some a = some a' → a = a' have eq_reps : (λ x, x = a) = (λ x, x = a'), from abst_inj (inhab A) (some_pred a) (some_pred a') Heq, show a = a', - from (congr1 a eq_reps) ◂ (refl a) + from (congr1 eq_reps a) ◂ (refl a) theorem distinct {A : (Type U)} (a : A) : some a ≠ none := not_intro (assume N : some a = none, have eq_reps : (λ x, x = a) = (λ x, false), from abst_inj (inhab A) (some_pred a) (none_pred A) N, show false, - from (congr1 a eq_reps) ◂ (refl a)) + from (congr1 eq_reps a) ◂ (refl a)) definition value {A : (Type U)} (n : optional A) (H : is_some n) : A := ε (inhabited_ex_intro H) (λ x, some x = n) diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index 5f73f83194..e6c39a7f21 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -41,6 +41,7 @@ MK_CONSTANT(subst_fn, name("subst")); MK_CONSTANT(substp_fn, name("substp")); MK_CONSTANT(symm_fn, name("symm")); MK_CONSTANT(trans_fn, name("trans")); +MK_CONSTANT(hcongr1_fn, name("hcongr1")); MK_CONSTANT(congr1_fn, name("congr1")); MK_CONSTANT(congr2_fn, name("congr2")); MK_CONSTANT(congr_fn, name("congr")); diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index c4de4e3d9d..5fbcfa7258 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -114,6 +114,9 @@ inline expr mk_symm_th(expr const & e1, expr const & e2, expr const & e3, expr c expr mk_trans_fn(); bool is_trans_fn(expr const & e); inline expr mk_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_trans_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_hcongr1_fn(); +bool is_hcongr1_fn(expr const & e); +inline expr mk_hcongr1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hcongr1_fn(), e1, e2, e3, e4, e5, e6}); } expr mk_congr1_fn(); bool is_congr1_fn(expr const & e); inline expr mk_congr1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr1_fn(), e1, e2, e3, e4, e5, e6}); } diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index 6a2ec989d8..c8b9e6aa21 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -240,7 +240,7 @@ class simplifier_cell::imp { expr mk_congr1_th(expr const & f_type, expr const & f, expr const & new_f, expr const & a, expr const & Heq_f) { expr const & A = abst_domain(f_type); expr B = lower_free_vars(abst_body(f_type), 1, 1); - return ::lean::mk_congr1_th(A, B, f, new_f, a, Heq_f); + return ::lean::mk_congr1_th(A, B, f, new_f, Heq_f, a); } expr mk_congr2_th(expr const & f_type, expr const & a, expr const & new_a, expr const & f, expr Heq_a) { diff --git a/tests/lean/add_assoc.lean.expected.out b/tests/lean/add_assoc.lean.expected.out index 0bf04407ff..aac3b3dad3 100644 --- a/tests/lean/add_assoc.lean.expected.out +++ b/tests/lean/add_assoc.lean.expected.out @@ -9,9 +9,9 @@ Nat::add_succl : ∀ a b : ℕ, a + 1 + b = a + b + 1 theorem add_assoc (a b c : ℕ) : a + (b + c) = a + b + c := Nat::induction_on a - (eqt_elim (trans (congr (congr2 eq (Nat::add_zerol (b + c))) (congr1 c (congr2 Nat::add (Nat::add_zerol b)))) + (eqt_elim (trans (congr (congr2 eq (Nat::add_zerol (b + c))) (congr1 (congr2 Nat::add (Nat::add_zerol b)) c)) (eq_id (b + c)))) (λ (n : ℕ) (iH : n + (b + c) = n + b + c), - eqt_elim (trans (congr (congr2 eq (trans (Nat::add_succl n (b + c)) (congr1 1 (congr2 Nat::add iH)))) - (trans (congr1 c (congr2 Nat::add (Nat::add_succl n b))) (Nat::add_succl (n + b) c))) + eqt_elim (trans (congr (congr2 eq (trans (Nat::add_succl n (b + c)) (congr1 (congr2 Nat::add iH) 1))) + (trans (congr1 (congr2 Nat::add (Nat::add_succl n b)) c) (Nat::add_succl (n + b) c))) (eq_id (n + b + c + 1)))) diff --git a/tests/lean/bad_simp2.lean.expected.out b/tests/lean/bad_simp2.lean.expected.out index bf39709a0e..7aef502857 100644 --- a/tests/lean/bad_simp2.lean.expected.out +++ b/tests/lean/bad_simp2.lean.expected.out @@ -28,5 +28,5 @@ bad_simp2.lean:51:3: error: failed to create proof for the following proof state Proof state: A : Type, B : (Type 1) ⊢ h2 A B = A theorem T5a (A B : Type) : h2 A B = A := - eqt_elim (trans (congr1 A (congr2 eq (Ax5 A B (eqt_elim (trans (congr1 A (congr2 eq (Ax1 A))) (eq_id A)))))) + eqt_elim (trans (congr1 (congr2 eq (Ax5 A B (eqt_elim (trans (congr1 (congr2 eq (Ax1 A)) A) (eq_id A))))) A) (eq_id A)) diff --git a/tests/lean/find.lean.expected.out b/tests/lean/find.lean.expected.out index a823e00e39..1843bc4dd1 100644 --- a/tests/lean/find.lean.expected.out +++ b/tests/lean/find.lean.expected.out @@ -1,7 +1,7 @@ Set: pp::colors Set: pp::unicode Imported 'find' -theorem congr1 {A B : (Type U)} {f g : A → B} (a : A) (H : f = g) : f a = g a +theorem congr1 {A B : (Type U)} {f g : A → B} (H : f = g) (a : A) : f a = g a theorem congr2 {A B : (Type U)} {a b : A} (f : A → B) (H : a = b) : f a = f b theorem congr {A B : (Type U)} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b find.lean:3:0: error: executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:24), no object name in the environment matches the regular expression 'foo' diff --git a/tests/lean/simp10.lean.expected.out b/tests/lean/simp10.lean.expected.out index 903a56b3b5..9e77039d14 100644 --- a/tests/lean/simp10.lean.expected.out +++ b/tests/lean/simp10.lean.expected.out @@ -8,5 +8,5 @@ Proved: one_neq_0 a fid a - (eqt_elim (trans (trans (congr1 0 (congr2 neq (gcnst a))) neq_to_not_eq) + (eqt_elim (trans (trans (congr1 (congr2 neq (gcnst a)) 0) neq_to_not_eq) (trans (congr2 not (neq_elim one_neq_0)) not_false))) diff --git a/tests/lean/simp17.lean.expected.out b/tests/lean/simp17.lean.expected.out index ce3f0ca925..a3ee66757b 100644 --- a/tests/lean/simp17.lean.expected.out +++ b/tests/lean/simp17.lean.expected.out @@ -6,8 +6,8 @@ ⊥ trans (and_congrr (λ C::1 : b = 0 ∧ c = 1, - trans (congr (congr2 neq (congr1 0 (congr2 Nat::add (and_elimr C::1)))) - (congr1 1 (congr2 Nat::add (and_eliml C::1)))) + trans (congr (congr2 neq (congr1 (congr2 Nat::add (and_elimr C::1)) 0)) + (congr1 (congr2 Nat::add (and_eliml C::1)) 1)) (a_neq_a 1)) (λ C::7 : ⊥, refl (b = 0 ∧ c = 1))) (and_falser (b = 0 ∧ c = 1)) diff --git a/tests/lean/simp24.lean.expected.out b/tests/lean/simp24.lean.expected.out index 07d65e5757..cb7c4adf30 100644 --- a/tests/lean/simp24.lean.expected.out +++ b/tests/lean/simp24.lean.expected.out @@ -9,4 +9,4 @@ funext (λ x : ℕ, trans (imp_congr (refl (x = a)) (λ H : x = a, eq_id x)) (im λ x : ℕ, ⊤ funext (λ x : ℕ, trans (imp_congr (congr2 (eq x) (Nat::add_zeror a)) (λ H : x = a, eq_id a)) (imp_truer (x = a))) λ x : ℕ, a = 1 → x > 1 -funext (λ x : ℕ, imp_congr (congr1 1 (congr2 eq (Nat::add_zeror a))) (λ C::2 : a = 1, congr2 (Nat::gt x) C::2)) +funext (λ x : ℕ, imp_congr (congr1 (congr2 eq (Nat::add_zeror a)) 1) (λ C::2 : a = 1, congr2 (Nat::gt x) C::2)) diff --git a/tests/lean/simp26.lean.expected.out b/tests/lean/simp26.lean.expected.out index 55b376054c..537c2ba9b8 100644 --- a/tests/lean/simp26.lean.expected.out +++ b/tests/lean/simp26.lean.expected.out @@ -6,12 +6,12 @@ λ x : ℕ, a = 1 → x > f (λ y : ℕ, y + 1) funext (λ x : ℕ, imp_congr - (congr1 1 (congr2 eq (Nat::add_zeror a))) + (congr1 (congr2 eq (Nat::add_zeror a)) 1) (λ C::4 : a = 1, congr2 (Nat::gt x) (congr2 f (funext (λ y : ℕ, congr2 (Nat::add y) C::4))))) λ x : ℕ, a = 1 → x = 2 → 2 > f (λ y : ℕ, y + 1 + 2) funext (λ x : ℕ, imp_congr - (congr1 1 (congr2 eq (Nat::add_zeror a))) + (congr1 (congr2 eq (Nat::add_zeror a)) 1) (λ C::8 : a = 1, imp_congr (refl (x = 2)) diff --git a/tests/lean/simp29.lean.expected.out b/tests/lean/simp29.lean.expected.out index 26a034e406..7f6ba1e616 100644 --- a/tests/lean/simp29.lean.expected.out +++ b/tests/lean/simp29.lean.expected.out @@ -5,4 +5,4 @@ Assumed: f Assumed: fNat (∀ x : ℕ, x > 0) ∧ (∀ x : Bool, f x) -congr1 (∀ x : Bool, f x) (congr2 and (allext (λ x : ℕ, fNat x))) +congr1 (congr2 and (allext (λ x : ℕ, fNat x))) (∀ x : Bool, f x) diff --git a/tests/lean/simp3.lean b/tests/lean/simp3.lean index 6d350997a7..7b6c655193 100644 --- a/tests/lean/simp3.lean +++ b/tests/lean/simp3.lean @@ -40,16 +40,16 @@ print(pr) *) theorem congr2_congr1 {A B C : TypeU} {f g : A → B} (h : B → C) (Hfg : f = g) (a : A) : - congr2 h (congr1 a Hfg) = congr2 (λ x, h (x a)) Hfg -:= proof_irrel (congr2 h (congr1 a Hfg)) (congr2 (λ x, h (x a)) Hfg) + congr2 h (congr1 Hfg a) = congr2 (λ x, h (x a)) Hfg +:= proof_irrel (congr2 h (congr1 Hfg a)) (congr2 (λ x, h (x a)) Hfg) theorem congr2_congr2 {A B C : TypeU} {a b : A} (f : A → B) (h : B → C) (Hab : a = b) : congr2 h (congr2 f Hab) = congr2 (λ x, h (f x)) Hab := proof_irrel (congr2 h (congr2 f Hab)) (congr2 (λ x, h (f x)) Hab) theorem congr1_congr2 {A B C : TypeU} {a b : A} (f : A → B → C) (Hab : a = b) (c : B): - congr1 c (congr2 f Hab) = congr2 (λ x, f x c) Hab -:= proof_irrel (congr1 c (congr2 f Hab)) (congr2 (λ x, f x c) Hab) + congr1 (congr2 f Hab) c = congr2 (λ x, f x c) Hab +:= proof_irrel (congr1 (congr2 f Hab) c) (congr2 (λ x, f x c) Hab) rewrite_set proofsimp add_rewrite congr2_congr1 congr2_congr2 congr1_congr2 : proofsimp diff --git a/tests/lean/simp3.lean.expected.out b/tests/lean/simp3.lean.expected.out index df175dcbcd..75b88dc898 100644 --- a/tests/lean/simp3.lean.expected.out +++ b/tests/lean/simp3.lean.expected.out @@ -20,9 +20,9 @@ trans (Nat::distributel a b (c + d)) Proved: congr1_congr2 ⊤ trans (congr (congr2 eq - (congr1 10 - (congr2 Nat::add (trans (congr2 (ite (a > 0) b) (Nat::add_zeror b)) (if_a_a (a > 0) b))))) - (congr1 10 (congr2 Nat::add (if_a_a (a > 0) b)))) + (congr1 (congr2 Nat::add (trans (congr2 (ite (a > 0) b) (Nat::add_zeror b)) (if_a_a (a > 0) b))) + 10)) + (congr1 (congr2 Nat::add (if_a_a (a > 0) b)) 10)) (eq_id (b + 10)) trans (congr (congr2 (λ x : ℕ, eq ((λ x : ℕ, x + 10) x)) (trans (congr2 (ite (a > 0) b) (Nat::add_zeror b)) (if_a_a (a > 0) b))) diff --git a/tests/lean/simp31.lean.expected.out b/tests/lean/simp31.lean.expected.out index 0cf34d763e..5882fd47be 100644 --- a/tests/lean/simp31.lean.expected.out +++ b/tests/lean/simp31.lean.expected.out @@ -38,5 +38,5 @@ Step: a + (a + b) ===> a + (a + b) Step: a + (b + a) ===> a + (a + b) Step: a + (b + 0) + a ===> a + (a + b) a + (a + b) -trans (trans (congr1 a (congr2 Nat::add (congr2 (Nat::add a) (Nat::add_zeror b)))) (Nat::add_assoc a b a)) +trans (trans (congr1 (congr2 Nat::add (congr2 (Nat::add a) (Nat::add_zeror b))) a) (Nat::add_assoc a b a)) (congr2 (Nat::add a) (Nat::add_comm b a)) diff --git a/tests/lean/simp33.lean.expected.out b/tests/lean/simp33.lean.expected.out index 224c905c18..5b2901b12e 100644 --- a/tests/lean/simp33.lean.expected.out +++ b/tests/lean/simp33.lean.expected.out @@ -6,4 +6,4 @@ Assumed: Ax2 Proved: T1 theorem T1 (a : ℕ) : f (f a > 0) := - eqt_elim (trans (trans (congr2 f (congr1 0 (congr2 Nat::gt (Ax2 a)))) (Ax1 ⊥)) not_false) + eqt_elim (trans (trans (congr2 f (congr1 (congr2 Nat::gt (Ax2 a)) 0)) (Ax1 ⊥)) not_false)