From 6329d1828dc9310384e686f448bf7cc152ea4a68 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Jan 2014 20:08:21 -0800 Subject: [PATCH] feat(frontends/lean): reuse name expression Signed-off-by: Leonardo de Moura --- src/builtin/obj/Nat.olean | Bin 13027 -> 12937 bytes src/builtin/obj/kernel.olean | Bin 16442 -> 16364 bytes src/frontends/lean/parser_expr.cpp | 4 +++- 3 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index 16e56518f9ac8053a7f38193f6dc2f7b45332a1b..6e917a20a95d88cc1500a1559e182d31ea49c997 100644 GIT binary patch delta 674 zcmaEy+L^kcm6bI<-BPFx>33n_L)PNwq6s1tGyc&oM1`FGO1wh1KP7rB3c>kt{}~IIv=D1~b;e4HnyMA;!Zv`HQGD`((JF z^yFUg6vl|jpTyU(rGZVEY%eY|`H(~aQwYQ4UF?dRO(h)|*|H&0vn4bp#|v<6UMsbc zZE~rU%;YM?c;Qr#9K#V1!KumwqOvx>QB+|RF9oq7UMNE_%YnX8-Rz^x!^BuHIa2lV zWC3N}&5>#;EJ_^+MV$y{7lPS6`M#DmW7TACZCS?l$(q`MY`tK~$vd*C(-6$*lb`EEGESN7sB6MI3oNV#c6QI?CS6a)Ig`)mR{6|BD4&mD zEg^Knd(eTt`(WZCB?2enYkc!Fu%{3ypTt6N4}_7N|vLvz5S0CPx3sD#8_5OkOCwiP39wh)5RWWF~QGp;}HXhKq0h zCd$Lem=1D)7|?Xa$=FoMOtu$KVT_) z8ZZc=q_(k%mm}O*fnZinR#!|B&ISoE903uWs!SlNVDmgh6~@W;RCPDMSCVF8ESt=& zdRe>?Bn1iFCIqt?qc4($Qq7DwgCuq?~r?(TA1U_masun5AIM43p8;^>SvXk{j%GU%W-QCia< zO=dWcnKezR*>theqA)2e?_z-3MKKGNL_%&rdNbzw5EVdHp}%7QfU zy)KwIK8E!Lyi`dG{*HDTGsf$AbQv@BqL>j5%J2M#LA1#&(l6r;y_#-dSkKh{WJ|JW zKMH3|9o@qE7+;L(AEp1xC~wyt^ct4i$cZh~#E7Cenb8;ps}clU+#}&S(XrwT9$}n zRqQ9SGX_Lnv_aG_Fb1RXbI6M7gr@3vcE}P5jIu-`qnsj%QBER*LnHSHrWsQ6#H=dlhtT=~Rew|5-vQsXjd;)m}nZ2TaK4W2u*akP? za7;I9G&t%g8{Li?S25?vN@5$zN+qnyds~V!=j;h$TL$mM6l`<4$&W5)vvwaFWy?xT zcg;0U%}$rYI9*3vy?V6@KBTaw?So|9O!ILtwT%{_Iqf(tLV0?st%5x!F{hTy7plYR zbU!V|p7f+{~7B%2$cdfRZ?Xvd@^t-*8hgdL)trd`OgC3y-?#h~!yHJ|3 ziB_UF zWjpCvXgNj5$c|{6l@mtV%c^86ZWhGj`AI$cD@xp=@Kr3yb(%Mtu-zVQrp?%yJ5_s4 zg2Jc5@7LZ|;hiG=#rzX^EZ;gtY>ZuKC~%s01T)^l zy9H(1M=Imvwwndx2!jPd`{%IwoaPUM_D@meE7SKX`xgrLVY{!C+R^W8aec{hsOa|< zqugJej0Hm7kCwv4)PcdmM_u9pO7mf5KBCM=QD0O<2eG4QzIL2tY3{;!|JvLGECj?( z)#b`Uvv}mx&TQd#jm0Y7s7A{+|2gkz)@2p(b0O#Bp9>46ag4iL_{C&N7iWl$1@FKq z^cCN)onep6KZ~r%-THYY{LCl|{(|rlkNL-7>QAUGS(kHx!}91|WR%WJjPmFW7-X52 zE{;Mr%%w}{S2UDfF^=A>Dfd!8woF;)y2f@{WSCJFxy~qy{0@KF9U6kKyh>MZei~Kg izp%C3Yn1CL_f8yQ*;HkGLM}3i!=(NH^0@^^Anrd|ieeG~ delta 2256 zcmZvddr;I>6vuyOXEAYq*6y}S9Cd(J(- z`@8q|yRmvtBkamG8nQwwYL|t=;i{!eaICS=qzf-xy8M5lf(^zAL#PLhv$ZybeTGL+ z+$V8A`b?QaWHcC)@hy`Et+>@R)&7G_XqR}H(7-Dm!4c-!a0nNeOSGfXaZKWI+-J^% z4t!wFoAi^EJ0+fE2t}hQMv-br)zMEY1trM7P(q|msi~!3S{dBIEn0^9fGjDz#eO`g&4v5uvF2KNUqT1Yd`Urv zjn=s^fETSk=VO$~i^Fh6(40oX_Y`=BLG*ne3uEmt3@c*2>IfPXDF)mY`vOGbKx}2; z36gmaU?f~b?SP4}nxmO;IY+)LN;z8ay|{(&IO^h;1gzu`C1MFhi8w;OIU$}f$nz2y zK^Mm)+#Wv@w09DgmD$K3D%c4{1%78l6SOG@n@A-TP4J7Z;KdxI&gAICwuEBPP@m{y z4dy30AQ|T;PH|a5UW{wqj=zCqp{gk|w5PlP=QSgd#16 zuv*;G0bHB3E;^DFrJjOo@Pxn^bd9RX^O7bi2muqZMqzsA+fx9PKu_3N~}w5h6U(MYlmvQot7Fkl{^aH(rOA{v=F8{ z0#JjMj%ui79t(CmY_J&h&P-T_Zs&BhPS$-D*E_u#hj_p;&u^==c|vU{{ma)Qkgw_v>62Jhl4c~*EI%iYE52XgR3 zOvoOE2i@)3CsO=W;%E3#jt#c*z$$LG0+BZ_%Bk@~2;I+Y5Jo#(<+gqr8CkOXRY{lnt$3Y9O&uy^pBRPU^ z&i#a9&mAE2aP=T&`(B1N+~}KcKTNVPA0ZUx9|?uI0~7pyXvgXPIVyiS3G;Dm@xSKg zZ@C~p_L_*4SkJcrv=Hl63MT$^V^f9#XFaD$7gf#>iYd=B(!+mGMg2(n?+~Z^D8K$w zxHfN+dY)25_659<*P;C;g>FJot_R!3y5Jm7yokf{8^>IxL2(qXNMA3ZIEwVH(ob>l zqv65b`BiWglg3?PM=_#c0$jq$1&#JwWEVwl6N<_HBosyd!fOTna1(nAOEvknfPQIy sh*OKatlVlAZ?YJj^6$gvJ~IJ4U0b2(LMy7mbzudbTJqAws>LDYA0b'show' expr 'by' tactic */ expr parser_imp::parse_show_expr() { auto p = pos(); @@ -900,7 +902,7 @@ expr parser_imp::parse_show_expr() { if (curr_is_comma()) { next(); expr b = parse_expr(); - return mk_let("show-expression", t, b, Var(0)); + return mk_let(g_show_expr, t, b, Var(0)); } else { check_next(scanner::token::By, "invalid 'show' expression, 'by' or ',' expected"); tactic tac = parse_tactic_expr();