From 2179e57db31fd41b611386de5edfdbbf12db82fa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Jan 2014 14:06:23 -0800 Subject: [PATCH] refactor(builtin): move if_then_else to its own module Signed-off-by: Leonardo de Moura --- doc/lean/expr.md | 6 ++++-- src/builtin/CMakeLists.txt | 11 +++++------ src/builtin/Int.lean | 3 ++- src/builtin/Real.lean | 3 ++- src/builtin/if_then_else.lean | 11 +++++++++++ src/builtin/kernel.lean | 1 - src/builtin/obj/Int.olean | Bin 1477 -> 1536 bytes src/builtin/obj/Nat.olean | Bin 15313 -> 15355 bytes src/builtin/obj/Real.olean | Bin 1029 -> 1075 bytes src/builtin/obj/if_then_else.olean | Bin 0 -> 573 bytes src/builtin/obj/kernel.olean | Bin 15524 -> 15506 bytes src/builtin/obj/specialfn.olean | Bin 768 -> 779 bytes src/frontends/lean/parser_expr.cpp | 4 +--- src/frontends/lean/pp.cpp | 26 ++++++++++++++++---------- src/kernel/builtin.cpp | 8 ++++---- src/library/elaborator/elaborator.cpp | 12 +++++------- tests/lean/arith7.lean.expected.out | 2 +- tests/lean/tst1.lean | 3 ++- tests/lean/tst1.lean.expected.out | 7 ++++--- tests/lean/tst3.lean | 1 + tests/lean/tst3.lean.expected.out | 7 +++++++ 21 files changed, 65 insertions(+), 40 deletions(-) create mode 100644 src/builtin/if_then_else.lean create mode 100644 src/builtin/obj/if_then_else.olean diff --git a/doc/lean/expr.md b/doc/lean/expr.md index 16f508b891..905353c7ed 100644 --- a/doc/lean/expr.md +++ b/doc/lean/expr.md @@ -35,10 +35,12 @@ eval s + 1 In Lean, the expression `f t` is a function application, where `f` is a function that is applied to `t`. In the following example, we define the function `max`. The `eval` command evaluates the application `max 1 2`, -and returns the value `2`. Note that, the expression `if (x >= y) x y` is also a function application. +and returns the value `2`. Note that, the expression `if (x >= y) then x else y` is also a function application. +It is notation for `ite (x >= y) x y`. ```lean -definition max (x y : Nat) : Nat := if (x >= y) x y +import if_then_else +definition max (x y : Nat) : Nat := if (x >= y) then x else y eval max 1 2 ``` diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index 74edae1893..a8a486f47b 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -70,9 +70,8 @@ endfunction() add_kernel_theory("kernel.lean" "${CMAKE_CURRENT_BINARY_DIR}/macros.lua") add_kernel_theory("Nat.lean" "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean") -add_theory("Int.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") -add_theory("Real.lean" "${CMAKE_CURRENT_BINARY_DIR}/Int.olean") -add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/Real.olean") -add_theory("cast.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") - - +add_theory("if_then_else.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") +add_theory("Int.lean" "${CMAKE_CURRENT_BINARY_DIR}/if_then_else.olean") +add_theory("Real.lean" "${CMAKE_CURRENT_BINARY_DIR}/Int.olean") +add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/Real.olean") +add_theory("cast.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") diff --git a/src/builtin/Int.lean b/src/builtin/Int.lean index 09a4b317fb..7ea445896e 100644 --- a/src/builtin/Int.lean +++ b/src/builtin/Int.lean @@ -1,4 +1,5 @@ import Nat +import if_then_else variable Int : Type alias ℤ : Int @@ -43,7 +44,7 @@ infixl 70 mod : mod definition divides (a b : Int) : Bool := (b mod a) = 0 infix 50 | : divides -definition abs (a : Int) : Int := if (0 ≤ a) a (- a) +definition abs (a : Int) : Int := if (0 ≤ a) then a else (- a) notation 55 | _ | : abs set_opaque sub true diff --git a/src/builtin/Real.lean b/src/builtin/Real.lean index daf8585f67..3fd9c420c6 100644 --- a/src/builtin/Real.lean +++ b/src/builtin/Real.lean @@ -1,4 +1,5 @@ import Int +import if_then_else variable Real : Type alias ℝ : Real @@ -39,6 +40,6 @@ infixl 65 - : sub definition neg (a : Real) : Real := -1.0 * a notation 75 - _ : neg -definition abs (a : Real) : Real := if (0.0 ≤ a) a (- a) +definition abs (a : Real) : Real := if (0.0 ≤ a) then a else (- a) notation 55 | _ | : abs end diff --git a/src/builtin/if_then_else.lean b/src/builtin/if_then_else.lean new file mode 100644 index 0000000000..4f023c92bd --- /dev/null +++ b/src/builtin/if_then_else.lean @@ -0,0 +1,11 @@ +-- if_then_else expression support +builtin ite {A : (Type U)} : Bool → A → A → A +notation 60 if _ then _ else _ : ite + +axiom if_true {A : TypeU} (a b : A) : if true then a else b = a +axiom if_false {A : TypeU} (a b : A) : if false then a else b = b + +theorem if_a_a {A : TypeU} (c : Bool) (a : A) : if c then a else a = a +:= case (λ x, if x then a else a = a) (if_true a a) (if_false a a) c + +set_opaque ite true \ No newline at end of file diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 62a7ee6c76..35b8db6c8d 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -6,7 +6,6 @@ variable Bool : Type -- The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions builtin true : Bool builtin false : Bool -builtin if {A : (Type U)} : Bool → A → A → A definition TypeU := (Type U) diff --git a/src/builtin/obj/Int.olean b/src/builtin/obj/Int.olean index 0f6d1e7a7968bd64e76c03f76145feb681153fcd..09962ad04cfe4d9054e6527cbdf87e23d32f4cb6 100644 GIT binary patch literal 1536 zcmZ`(%We}f6uowu6ro5YKoJ`jeW9ulsYR8#DM@Le5<)7U5P29USWIS0#_6g{HvC8V zv3?0Y*E1PAgi++&_qjg4c9Ch7PfVt%`h=O?6mv^I^gP!YRob<(wP+?|`(5W_ot2ty z)tuz#+|s5XnG}{(W>iV?;nzJ$Uolyj%$l59xw2zhjE#%FEcE=FDRPoBuu>ITYD+DI z9n}_A$0|+fy0FS3(|tm|VUQ1UgL{BK&X_H-m5f8qxT-SXk26wpyOIG5wo>Onk8>P( zaa(8aNw|!66$;3W10H_g`v`2Ko9YSq9ZWTKq=Jz|MEch*#TIvguzqIoM^D;yEA6_KU3XsYkcmOJ5Y)%gi$Tw--NW^g zn!3~f*G1?HzZHnQ)BTfWfsL zfaZD%6KyX!g0>g)Fo2D|@IBZMl4nKAo}Fd#l3;G=0N$!Mh&{GGW-IG449fWdh4UZ) za-(WeUBbNXH20;{KiNrwA&#K*u=JU#7VfOOg)!b;a1d_;G?jRyhLhJ)8e6?A9-)ik zCs-J!$1sPihaghkk^5~r$0^fyOkZylZ6L6Z0~d{oqX<;65vVlx87CvDWQI;mD z{8+vOpYd+ij>2l?ow3i%86S_=b$f6=S7wWek(9{WgP`s z4}+}BRkA}gWbraRs?Eo2GEEa^kIfc0)ZjH{wzo3yUBp{?7?2iv#_*$!MsSZ~9R>{f z&cR1P@Z6-l@?;ad5ts|=W3{XeW|wE%Jj;GegLL2+GtqHCY%1|gwI%e JA|2z`{SN_*&ocl3 diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index 38c2125bade3e381d48ab516f5811f6032c416e9..afbe1a8d74b84e4a5bacd2085dad57fd3217a073 100644 GIT binary patch literal 15355 zcmb7LYjB-K8UA*^Bu&$V0>cb-28FaF1R13*2n@8P1+1q9!5;-=0K-Yn2^`3!IZ4`b zsai1=u-wH`WC}R=%NsKlwNwziG6NMVpv)-cqJs*9KZL)c`#kS=_T6vKmo#)_-QD-P z?`<#V%h+(WJUUbxt|r+(QybYhR-a6+tJX)W!^x&{J+T*-CzE+5u>)h1NqM+do=EIl zU%xN0LNYK_8=kCcDz#UtLy2f}bv0?TWlScf%??P% z+H=OnoXl1X7osuj9?tIZXxkx<98F%(s)iY4ch^+;I?x8C;7lslwQgi1rfF|$j2Gsjw*Q7|eXOq10{TEz5R+AB zjuuM|XuYO|OsM2yVXCafMd07O(Ewzcs35*a)c2GKs7{oyzV3DZWXk}`UwWiH}fwUcg*wV6O2_~t! zbz!mGDaEpcbgz|?C2)NTlumXTZ@r``VYaUk5NEi7F_YJ1p}VnOt>i)%LaFp|AY*k9 zqtk(BbJAyZusQ%1qv>l!yBdw@rK`?JTJ08$h25p-b+#h3(K`+e<%nOMDTm6#6V?9e zaBUIJ~|SvywGq(lp$gDkCgBycO?;xVxnjftqTNC$|r zyIs+%x+UOW#i>ypUn>3HMzr+TMkniIoXo1vp%||RayJ_2KQT2hA*C^}V2KVm7dWO} z(~brrzdUa?R7@6tEok|nek7UZy8(c!es-@BD(%4;Mq!avF#9w4NYk;f|j0x;9 z+L_#(|2AU^2~?8aRyvEi8ZK-$3qkQV&~u%=V=f;j>*dkL77(%Nm2ou7 zdd^tt6-%B3)nte3qMtN;_X5%tEG0|sh$X4WG7MkPK7pn)XISi;fnjIg&S^_-2Ft0% zwcsZ)b{)G-#tzEQc3^a>uB$Ponw`}6XBY?WBrn>&$#OIrL9W7r>_jw4obE(B5ZVh^ z)FZY`FQsW%9sp(+>(Wc?=J%Bz%&}o6Jdff2!c`0blv{vWpahr(K(|05I2G#-c!TJ* z7?om_)fF)rG-<0d?n0#|4t|9>_ELh6BP{12J zR#oC1Rz%Py>Z~`x^mScw31b=~AM1l-Zhs4k@Br{~nUC=@Rg|GF3CBHJLR}V29m2ZO z4&v1jF;^MJH;^Q_&|^lw8ZAfCTmoBE?3y+DRy#(*i#Se=0Z`9=2fvb8_A=<};W)B{WQ=K(K=BNYvmR$E7(9kT@=B zPSwK5dLk{55k`&|a+=6(!QL2BIa%je-AW3fF=gysX_ggMJ32!01ZQ4tDMy zV6c%rv<+j1C?#52?gmU29*NAw0ChI&LCuvJIkI`21o`j-_lx6jQ(|V<9?(VQ%3K~e zQ}LM$6t+j|#Zu79s-nY@xq^@x;zLlDKbXaAmW}7rz)GTH zQAW$^bv@wGY2M(H?>GR2W0TpO4-bYX8w2P#nu)?i3^`E2v5B@R5r&3K)9uXMOh~}c zjm_5rE4BoEDSq<0jPI!(-- z&lL8^V-}TMC0N*)VdX0dVR3l!0$tM|WrhN;TojuIL z3G_wp61sBIRk?QoeESS?o7|}DB_Qo=5|65wq`e)$S2V$ zSbThNCXK=15j5OBve@&VR~`VYCtNPJ-KWJZnl|_nUT5M&p&j1`gS;K*b`3pKMbN6^ zOyqcWbJ)Qy*BM_!O+6x}lF>CZ+swfaXD4$bS!vmm1C^WxxY@gS$~~?J5diwSYiw)a z3{2ikMWjxv2TBf<$QhWElpI|{xtW_=!1OS1dX}8kGYBo4i*R5)Bl28Vl3AXbwTgmY zeDb#o-JCrPl;#7#86|ojb&t93>2F|aG7NwJP&VU@lq;js;f+*hA;r`gTG)0nuimZQ zd)TFIat_Y>*659tXMAfw7T(qrpLxW4&XwLy;`|L%)Zf@y$)#U=lm=AvUv#OJLzUme@fb3Ma&jIti87$HQV0JG@ zm-~Te5$aAX*GRpUqOQ8F1FFFRC<}o|gU84U#JDg zw*Vq<5USP6NTF4rTmdGUF-f04HS3-i9GvI2=gDKGzJc&yketaCeH*ID8^})W-p?-W zpfzuoU!a^Uu&vn#VkAsrW%i*W2<&aML*8w!pJckp)$>lwNZ67%Izw|e%{J)l?B~#} z8eU@HEb6I-=E>YXtgOjfbB^1ySR;3$bOgLvT44xJ%1tx&k6YQ_kF1ucY+eLEO>FyI-Z1t6n7lAsk&)93SLAmd z`?9F%h$Z%A?2TyuNJuYQ-H!IVk$q88?mmEIabl-PuNkT{4S6GIgG&Q%Me%+^VMqIn zz^4NsQ{VE6Q5sR1Jxr9xn3GSP-pyzq*2(7 zF_@+;6z#&MQJMars`~ zv=xGf*f#46E_m`u52p`(DEJ-H_`V-)$!nC-r(F5XM@~)c^$5B%|CzuNx2_t_eYR%s(cK2Nzx7g%|^mL zmt?#^Clvs~yQ-UqA*3?z14>4h2y`DRRmb~BtNr2U zN{+eQeGr>XKM(~MqAtLP+<#^P7okZPAu$%x)iDw%;evDxAwF~@CVPuRXW9|S1t1C? zS#0!UZn}m-U^~e#>MW6!7g`XnjwtPLP4+Q|1}T`PLC%nA37FYuNEBc?8jB*TCijJYD(h;04$eLn#( zOgLv3emYuY7O}>na3PIPiGyW;0*Jfv@xR*9v9J+?8J^ zegz`FtEXGh6%cyCrzQI8?3hZXdu0m)k3}e*;-{yMRXU}z866UXzkwJr?r*jGJMI47 zb<-&>|5^b*H4kGEF0~wP$Yx6Dxi{&}Qat&^uq@&B zk05ayxKN_(9+b$*^-wOo3vjBH*}!gIjwxpX_k}XM>Aei9t%&+|fJlCjK_t0JLt=sH zPQVY!82A*&B-s|=1M_}Cib!SAfIk5BSlxuFK*+?G)D%~?bXTiuliY5s3NV3XY2arG z(VEAL9+~?5{WW+-`HR1WDhe(tl`Qg)=`v8rT2uMt&loS z>AnC{yBQ#mA3y{<@LCo<^-uq;J=m-mCEAmLu|i8iHdD`bh76DK%qFw zqyo4wbAJ{?#_f)Q{Eh>W_P^BZ6--Ly`jdA5jIPAltFD*+C5|&UX+HpDZ&9ro2+%2| zsk(u5hij5;)M^^tptdmgIOz_8&9&u?qU)7>cw%K=!2#AKIogA0!mE?Fzrs^}S(C{S z-;t+pdm<@haCo{4c1$$1GbE2HtV%#4{y&MY0rIv3r0>u`xk7~LouGOTO?+W_yT?sR zjpO=+f5iG;@c;PIpq68Z$=1cAow(pZ6`GPIs#=yYps{Gr)AS8L-QAfLKa9__U-LN5*cE z>%4!sk-DfSi}j6T?aSb0%taf^e1A^5Q2c|Tdxi{$?oU_)p!<`{V03j3=Kgpzgylw{ M`|N0CE&ky5|M0;Kt^fc4 literal 15313 zcmb7LYmi(;6~5hfXLo0Ll_e>q#Kg*G0)-(ap{VdkVnUoGD1}7P0u+|n-3ghvnN4OV zAw-EW4>aK|BuGSliTXnXDGUgTk19(*L7+;jBtQvD6@@>9zoZK6?>l$;^zFH`2`Q@S z?sNLQ`kd3Jd+tt7)N9Rkjfr}a{WFb?n(_Fa%gEWV_ zamz%6dKOVv0ktoO>IBXcU9vPW4r>umOL@>6`+gk2#_Q{nKB{zGJ?XbKEJ#eh9hHu? z7fnu1I2st1(HM4z*qwv61V*H2@{E>cGSD!Ck$`XPdqAZ)nNonvz(gDWO9o3FQA!au|9M+2&jakUxNig7;9E}EQh z)_yB-{|&hL#gy-3No`xw2fTr)En{ON&FxC9;7zQ(4uDx`DkZcRpfPi~Rg036-G;G{yBxi839gNv@{xUYrd(H>n5vJ|CmI{G zgmD~f#aBxmqm*D2{JXq>5zS)Hw05$UafuY+&=Tzw5UGXAV`4cP6RpZT9iS?jnJ($o zoeKC@b7IstFOdG+j<<|7n(fvkC$sFc9D`{HuLhiP5BaCIj7~{v6w}fO)e>-)qA`OM zoPI%=WDIBGR(+j27>I+W=|q~kVPhsNcbzJ9th%OIUl4B>wYO(@U1YyVa#{yj9T*eX z6SOm_Ij^`LQwX3n(%U{4Wi>CcC=k26(5;taTzIKs1- zR9s5Rc%w(ip06bzD)=RIhQ+xV z74Zxt9g`V^}z~zYQE0}z(7gg1Z z2}@}gGI*74c1?T`3X5p7UIX7(ROKqhG)CUn$0ptR79`D8oK~aW3>2(SMKBkuVp>{yMN+%;%B~iK_Q8kUoe!;j!!Fq@u0c3!dkc3LC|6)-bRoty|UOfY&y0V0EOXrlWs^-#C zZE9+AtYEMDk6l)0`=^@IT;dLtnt5BY7Ar65Zh`^@yQ*|3_-Q)+04qqh5?D~-)NnqK z0+-_EmSJ}z@W{HPcQ~@HISo{flCEKq;8rstTboW$d@o%;#*J?YI#VFCU@A zK14dV<>2I|ZJ2{kMy;$y+BO*qMY#yOVdG{lsVB@33Og9f> zoehw%=n7({5k7-~%pR6}aTeAV7DwhvLVEZ|pI=5Zk>puqrh9M|aH#(yIXfS3g+w0I zFeq{slPIO)1z2*8)X>a}VPz`C66x&bI!YKAg~C%rX#yh>RYkBm79$ENN7c{=V*9gZ zg;`8n4jz(DhNIjqYni>aLc*w;H(P`PKq#9`JMSKpe>R{fn+y`M*;J^+7?8TlCMsAZ z3=LJ&CMGUfqo0*f$hv~#Ym(~&1qp$CjRY!n6Gu#C(+%*+yU?{CBVBA9|>*%tb%3( zxuodQPi3r;b|)bfMxoRdl$$#sm9DQg%&iXB?C-%>LL&$eW?ag^MiX#UnV8!sSXaUo zZjsaPhX}WVp!p%1J+8@W7WASjSoZixFNxg(b3dBpu1VsOpCB=sfYfL=O9otzWf^yF zv6||84q$FN7USe?5a6j48)aXlV-=XOBkXl^W@j%he&nAc5EyUZ#?<6@!QWLMzgM zq$f4fcR;1sif@rYcNnT6Xgd;{){1WxT5%ZU!|JnLk;dyHm)mnQjj1+)5=wcnn(@IZQ*7`*HE+5;TY&^PeAWa(a!7vB)2ob zdP?}Yu4GYpYSt_YdU54%Pjqwk1gtdg0xmLo-*=C>?&)uIOS>Mpzkev}c_XD}70?TB zq&f>OX0il?{b*!YZ`Ljk#qQt%uGy#h3oNAf$wGTmHB1%rnI5KW@mJHezKC|bWZT5qmV$*%?} z+MpKs?pi?j^Nq+Cz1DJ9W&;Oxs724p= zy8&Jj+Y%Mn1M$G~fDcmkg2?7w_=pIr_{)xkKjdZOWj|QD{P>s3s;ZZA<#bCuLkkPV zOIH;y1tv-cJ`323i;+l~wq*p(^Z1_!L?bwUL9kyS`I2jUm9Q|rIhT!>UmWaQj(r}n zmw-x{_^3Q6HBFmEoI{aTOipr zpv0;u+yGisW&0d3SCm{^U=ccIb}t7W&jS{8lDPx-y#f??N(o41TLoDS3ZTpdA_*=6 z>o0bg}Q45-*;hn0DiGf$5gGICDr#gLX2#T|!`p+G#G+GetFQdM5=7TQyzJ;ATx zc9{yuBS!)_67YOrUf4sxJ_nQ^FvLeFDmNzE6D-~fBzc2SsV;~Fx)7M>Lv)Rpq*8F^ z1%>nRoq6(Dsc#@G43fpv=njY`2i=|8{XV<2gXCW~wgPv!dVX0oy!gO*lv52ojIsR@2r?oh_xqTW<5{ec zQB_4DqZNYKS-EM(J9%HkV90M8ipvlEaNY+=slQg7_H;~234b@bvSkOfdyrlFRId1> zE+h%%?dg6@Yf5Dmo`xPSk9v46Gi&{%JnBVtt9=T*Eit+E^en8j=j3ClxB`)a=Y2Bq z+h*2c{lIk3RrU#>JQ?_zmos~*>T?L$A>ctQUbClZzzpLww1o#PVf@eH!ra zx5XlS8dgw={~YLPVB4qjhOy6s$X{u=oD)(E2oOlDkLmVB!r_|Y`!e=Mw0|Qc$~4cq zN&B3H-0eW%ft1-PlB-8{hD7oKk)%0FSa{x$*{MDv@aaIW59`Jt3qGETKdq1iM!U?V zi4GBwT^#mVG~CB-R|xQnJ%EsW?*>sKrN=-*b(8k>Myf=diC>xq zADlOU=s9iAnE4tF6ME<;yD-k)I|xD(9UUpJj;zKc zsAon3(43Sa`f)5x9ksNt2)#=6{rQ$!Fdpk6FR1jRIf<6^nImQD6Uk&xBUV*Vo#{Mn zQO?tJKZvj^8n2eDLy9S4K{6~e$Ewb!TlZq#MBf|LHwPc{26ayy4GC|))VW5Te*!@b zyFbJnI2B3O{6X9}~;xp8hF1@GKbAEynSIf6M5~v;{d-*nJ2f z@h-ljNcWdI%ctgL_`Gy8zW*kXB?_jSnF=Pvr8HpZ9&)BSXnKVvECwvDcxg>a>9esu zJIc7?8n|XEk1!3uIKCD=+K5R0`@Ube>0H1$yYSP|BD07!W`v4#J|zy+0L7EQPR#Tx zbj3D2Hl_O*W@kXJ^lG&(sX)rKiOF=-HHn|puM*+q(Pr`!S}(Mc6m?4=#ADb<;6v~1 zQa}t|T=+X_@IdTrfv@xR*9s-e*p;IEH=x9)!E`&i0zxnNv_xN>9Z`vNFKnUX(L2%> zKRtD%(w6e3cZhMH0voaD@3i}S?f$`a(-zhLBfDn+b^{t&_Bgw=@oaXditnMWr?8Ho`%GBm-v1%k?C@;l$e^&CTn({OKD|aEXw6k6~J3qJpBVgHe&%J_Xp^Kle+(J-5?HH{4rFKN3FriWQKnkCv}J;F}jqJ zJq;Z3hiA0=EV?s@@E6Voo9f2twP+rKXtGCD*Aq$M6Bx)Ap_7it4tZnBA%ey7BWPGn zd!&@fBYQCQv$B+1ChMbpI~-tY*W;&;PlNBo;gutO0`eyOt%ck0q#LD&!B2`rIwaZ0 zKlkBTBmH&BwfP;#1pJZ@s_AW%Ot<+-jHT!jsu3#@pOUL{F^jJ5W~Ev)5J<2J`YR)@ zjDCL@{Mn&IX|>jDH{72h6uXv$z4I;i2QVZ|NxY%$dmQs3D$ezSW03jTi|C4Tz2ti7 zKMI`7z6;2sMG0mkKqr^3JcgzFT$Ah=L@NoT;(Fq&tNo-a`MMLzk)n%~d}3nd1VO3l zA{*@yG+~kE?XU3kKr|WRyXEQY9xmAnW=s!6u9_ivRH0u5f8zf;a*)?SfTG zpnIVlLJt5YhmcT+>~u(_I0Q`WetOq2kSvhii{kz$CJ(7Bhw^5S(|%XUVdbM8NrRCf zUw`31P2UGrZ0w_XhT^CYB|CaM1uUP5jQQfGn*16ufQ%mu-GgH|bbrPg0No!~1|#?9 ZslmwonP@O_f7}_2u&&x1Uxh#8{XZDw{1N~F diff --git a/src/builtin/obj/Real.olean b/src/builtin/obj/Real.olean index 6035111cf16143518b74db6f58442cf473c83ca8..03fe91b75148aec984be29c6fde81236103225cd 100644 GIT binary patch literal 1075 zcmZ`(xlRKy5S?`r(jY_ugd!9u5RMRWG&B$i5J(6q1wRmZSre_;*l6QWQPS`cbns(* z34XJ?>_M<1XFPs0^XBlHNJ;$|MvBtqg_CC!TY6HlRuQGAp|qKJt1Z3An8dx35j8y$ zzOf{uP)fW- z$6LJvvDOh8-Z>)jpv=AFRHu}}R9UKV_@hjfoJTSUXlSgopyZY(dQAU9)RXi8sMt(q zQN?DTZEi9f04g>?_)@VsEZYE3v2iUaQ#(87EKjmH=vf)@{r;Iikjn~cnx-*Ugo0vu z3&KwXAuf$^RJp1xzGHEn#VzbB*j$U9Svk@m;{w3i9~xgdjW*K&Y&A-n*=l4|8W|Nd z(+v@E&^EwKqFD}lmgbN9Hjhjl;_CQ+zqsGXQ<>*=Q1H50@H(CObBYFs$uM?vafd|? zvjlOS#pPt?`o~aFC6|6WXSmufMAd2x747~O38!AU5Pj(Ajvv}y!C3lJzR8Wd?wwgT jCs!GcJ9xA8^Ry?T1kBb)-R4j<#!9P&4Zd!sdk!{+OM=$;eZ~Djj zOWc`kyB}y+W+#)E_a<+%R!d=qN=wK`pkCi>>flADMrz1skHXEz zv2`G{5@W#G#}}YyiYH1tWgt|>4V)dM1i!U1eOA^m1QR&~G@@9JPyix{@dz69TA~nk zDPlLw;Tb6eR9Y~yYzVpRSULz<@?>7}^MObbc(hKqyo~@4x#eqOYc0B_y@S_@u3--t z+b3+hicQqChCME@D^+Y}ceRC!OFqpR@vc^vW}n}sHL`5UTR)OOe$fabjD3Q5W32{Y z=i0o+=?bTN6jv!kWL{8Jy2_hiCtI}+XP-Ys8y#+gc$(UOtF^|wmBzf4E~3e92C!&{ z!0QyEs_2DhWz97xct`*963a$$l)qT7O01m{>v$6XVHy$oyS7!N+nlmYi_&#Y+x}AZ zPN`HsOV3{BKJCrg~n$5NU>P=jO&!afLy zG0!rCg+6o;0u6+L2BPVa(L(JniP{MMOv9WsE;7xWcEyTa+jE6&wsaq(ua3%q|3&`H zMrq0>SAbGr2iO&O4cIJ2wl-U$g&aXp*CQ|RH0H;_4aoW~K;@a5UVzImY5~gyQ)yVr aDp)om literal 0 HcmV?d00001 diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index af9437bc819fc3f5cea614d50b6b7b9d2a04e86e..e28979830752ebf6a26ad285fe770056c7d924a0 100644 GIT binary patch literal 15506 zcmbVT3y_^$N5ynV8P@3{PhH zrRi-CriYz{j4v*XPdNG>iL)Y&r-emZm4ySdZt#G(uWIOWV zEEio4*J}7tgE8{Ta}mupOiT|?k4-dyQuWW((gf7ibXk<~PrqJ^0bm7_}U3)Pb12tY%#CSBr8; z21tXyZZz{aXKd%L@v&kG9qr~d&1jK)`Em--L&;y>BKZYdGzhv2TP44%G)5_ky<=0; zQ)bW0GE%D;xG9>Kj+CR=o(-al2%ZCQanNorp0aK|vZbb-;<20bfw3s4)!E@4MLb2s zxx^rKlISG3487f5Y|(VC-?I_cu za$~SBP+x8jt<-1V{=pLc<=OO(EH8FOYt<;~e30psB?wZB^8s2^3^o)9t2i{gH_NvV zTPnfm`0MD%2UjX?JM)}LXJdn_)J0o$1ryeKoXx0US|~;9(_&=QdVENM(2|b)+N=Z6YtalO7AELm#OrWAfH6I4AwLn=3ak486 zVytBAR0CHt0&DO`6$t$`FH0RyYtSh5f*hNz2XZi2r-x0s=G@0}-Kup|dSb^7~w~vf>037H;OBvXy>>)@45>nm* zF$xDio0XdD-mCX9JL|MIBM+ z^ha$unY=0s9;Ki+vvVsrWQWmof)AJUt;P6QsYoK7@JHg^oIHVNS&2E)h2optg61F^ z5d_o?s$)BMZJnMRZeZE+qL(~FixH~}HJ?K4P z3F)aYa+qu}>9N#=WP_N+?*EshL*R59nf@U_N%fWl?n~fX0ZPCd01hPqX~sk7l*WLX z<-Oi|g1jc{OS3Gcyq!|s2-1@BZ3*0;zykmwnsRfF6_co}W0ZFQbK;`)NA?gzZA?sW z#XnoxgHLN+bO(2VNKxJI&V1NH&TP{7^9YeJjT$HIOoZEB4u$t*CSF+y;j$^xi(@^l}=E&32C z?RltxU}mI`b)4Uh~=qAIiR1t%HceF=O&KzZo{0B5z{GyrD$AVWZ>tlvn00US?~AmAGTRul*wXhVth}rvb~vCX3M}~J{oBQ=m(VO zZh(^L;|csL1D)+;e5IMiNZew4%pO7jHtJi)EY2rR#uyV7euOB;LV$FGoc&2WON37) z@Y4VlgP#$|Eo8|Wk0v{%K)fPY=My%mBqi3*lSHAcL#dK=B--b|S)zSDf%h2b7ONB> z9xM*guwKP9{jBx0@IOV6xW%9#b^i{anErhNzhIzSOanfP-frR% zMZp4*th*&#<%=(3NV0q>fe!-gj+G0AEA!8$fuDJn2(AhsXk@&@RpZ(qB5XMGxBU zQcqpg>tj67bYQfOrr)CwAM2ePq?5iw5EzBAqS+leu0bDbUTYIv_^=^_t%IGCXUdyi zI4&4z6)1I~Q8a%GpiJ|aLGDT&!9dPX(8y<6=U<7Al0TJ@$-T7Iap2HDu_k@fdgSS; z>vv+Kd>L@sU6q6&>ywPYQhYtm3G~Y`fQt2R1C%B(Ue?!#b~_q{10ap_#G&&ujo43N zXPQxCefSsa5B3Zj@lyy*j=U&P(hZp&G<7yaMGCNyBHsn5gXZ@DN|7f4O3?2E6fP_K z5S9J`dWVvF3Z#Te_3C8CA?hgqgcy0kuz5SMq3Ql{_NIfSlhqTv@@W)XUyP@E!Jit_ z-(r_KOZA32JOy;A&LENMKSZxo|B*os8|Rf7shp3Y5|ti2cPpvjA-^RcbD~B6{i}@y z|JknJ^m&P1Y~e5c=v9tT=>igHBz4mI8mVFY-_S_ue+MX~x$BV9|AAil`)PyREu8iY zz<0OvcfoP_yBBjIi|T{|8-1N9DDEbJNg!D=gu{<*jNyO-rx~bpkb9Al9=Vs3E!l|P zDPaI6}W14u*doXuPblQ^>WG z*cL{EUk*a0`zl-u;%{>(;QgUO4(T)~pY{MpRwnEJ!LtnfzW{Zc^$UO-f#3jTn+X!; zLg{k!4rvM4Y+~)jb5$VHmTpMb&n|R`*f%Y-zCqP2EqH1Q`#m1Guz;qX%dO*M(ks)Nvga?wRP_LW5vM zR;hIl0;J|aX>SrKO?|23rdFka?|2LgHOYZ^v(jyKmWCVKd0tj1OnKIyY#oygGWuwU zqPj<@3Kwr#;Fo|V3;Z%b#lgz~Dh}oYR2=*YK-L-es{q%L*slTfOAt)0nlnJFlQGO8 z#u-x4Jx41EjaKSpXqh1pb4q$5zCdy>Sf_S5GBzGbSJN^CP3C~*2y%>c!8l$YIz&JR z?&6hXdjAvB`!b+n=fSIiY;i}fltaSXNsJk=m^dOz3(rYDZpb7hO|yVR3H}Da#RPv7 zAU9WTp+WhX>|F%#W#WX55ei-Y1_HCa_&FNbDe(}F?jcTHg5mmdwBNCR?jbzv<#RS>8PCMd1z&yO67#yAklwYKY1kqef z>;hw$oUb<2kuvIj48gmKb*>jgZ(UB zYmn!tSb+wfBq+G6t;sJ!b1|CVK~t7pe9`;r7LF97#Bl(q`K8um6h>iLQi1$h%)t34 zHv@-bVFdvnAY-GWKBCcgVcUDX5GN3UF_K@vEu{k;A1ecZWSNjVG=?uJwq2NWu`-A$ zStmu~%+)n}b_^NC8>3TJA}mc1$dI&zX;bfkprgU@L3(8J?P&*d8lD zxkzjWT2@O&@@$jQC<|W(Y2lLV)^i#i`Z|Kqe))AB=%6062G~7?3L(r_%`1BCS;nbz1dlhGTndza4v(@E!}Wwt zYSCG;R`P`81Ww)vTJBAd0UZ1;PZ!?!TZ zs{9T-Lt*^pcO-=vD5-(1-8MEJIqU4j6oxkOl*T@^`M$AqRoE(0m(A7I%3TStB+}g) z@*>^cA`&M?er}sdqdFuG$1yp25fAO<>?+Gyx>7C4DG^D5rrQdzMsfBNv?k{Ttt94( z<$f1KndWlsb#G=*@DsiyX>S)*FCeQTGX!g*dP&w(erJ~74>Xo&zMRdE;Q4TD%FNm; zM`w|vm@(d3m3!C-iWT4d=l6htW=gef=!hXWJv=jAy2Gapc*!Xi3|!t2=MP}og+11| zYXDMS`*iD+D~7JE7ZM+h_H8==s`xP!Qy}p+JU{Bg)h*V2%qM`aGU(Tbd)dR7QCw-+ zfMs~W3nD6 z-^8LxN(G0cX8ukrM(w~D1O#DEc|nnhX54`1wIwtIcTO---lVHRBQQ2 zN-`$Zxr9me{g_x%eFdJQ>MOum@6EN}N%_x96b0xpAW>~~dc&Q>G{S*t@G_d8I_lnt zdpHIIRb%7;h1SbTI2A3mbmyO z0{KyTm;`9Pc>(o$OtH;#4}PFSWqw4hT!K#GmzK+u&+JVzc`Rz332OWl3U)zhZ@r$? zRu<=epjIx8^s-rW@QuFX?X9$a7kUNWY*6J=%62H~!V*(?qf+i5kW-O~7nkmkb^D_x z1S@~19j_vief(jJ;mBZ+FKz*GiNdWWgR;FZMyM7EoW>XV{Soyg`Xc{qnt6I(*p~P- zuDB+WE4$*oN$K|`@cjl>u4!=v&t#Qpx#G`(+|CuZT6f76cJgnR7nr<)Y2-83p51Ne zl>=@k7~*sDUA(FLw2gU@>~*8RnGZK0UB@G7qE{t7y*T>ZdV12453*u=%}bHJ$*{5(Kys_y~V%iendUe#xfd%goOZ`w(k z2B3bGf5r&#D_=wN4XhoW>3Ifb+>i4OitM5JKovf4qA73;3Rm%5`zI#ti+%G?s~OUA zl5I?C+DA1iR?MbXP>cJ(Kx*x*UJs$? zxQ=#%>|q&^V&u65G}CkCsVEVmHN6L|JO#WZ4oT0s)Ck}OtGbPfCt?DwmZN81T?|${q5tAlT?V%K7-NKd)B7F~pnD3iVQRWTlA%pW zn{swWiQJ%1Avf46&kLZzIbc*>VL~(teV0Q+kiFEVP@}-Q5Y72|owC$my(F%#0yuzx z${z=E>6;Y^Y+ddr7?6ck02M;tGpM>=F=3!X5w4zXO$AxRYXzFi-3Rrn+Tq)qN1TW zaO9@Rs%M{vN$?@w^D2FH`JW=kza$3^R-EbvXs2}vbgL-kDUk8Hm?2$#V-$#?Q+*Zi zbof2i;v`x{-!~?=$J+R9o7c`ur*aY*Fnww^y9!rT*8_CNt?^0wLx8gQj{tJ-&HME* zAyf-R9KxlP!b-|;e^Fg8BuG0KDMZ{;Hs;*MUH1QZeT~4=s!Ill?B!qR#4dYYwsgdz9Ou6#VC-HC5Q=;uCNN;?C zJH>in%nlyV}P>@>Hz)jJ-oghLR%U`cWe<96%I>1FiyWQv&UFx!> zrk&!klk|bHFsRj8^Nu2(sGms;QYVQ{g3B=4MM*>x@rS=9_Mdaj8orT%w2G=MQM8OT zb`pI>hv|sFg~3Uk!AV|jO!fro-PUQPe&mJ^XY{*^scl8s*dDD_qp0&irc;(6NG;9+ zXi?EWra)N5srv4s9IRV@!RYv#Q!D#dDsHKXQrTWw36!r?>GW%zZ#A5|dqc6eC^(OZM2IY$sxkb{vrRX63Lv#AYKW+g8+ST;y6 zPAmp3CE(=%mGoBtyqE!fCBO|UO8f)knrAqE89_Ak#dbi6^fKZj1pWNtV6nH_NGU<5 zCPsFR)JKWrm{U`LS%;`eePD8WVkmk_Q3(`8gbX$p-I5Z$9iS>q9iX%t063TN%5aI1 zvem}D!FF1u30YxGxCA?kcTZ2`)(2wJe+ZzsH4;c0_fVXxG1}LImISGmvL_jkgOsaT zIQZGD)Lit=-^1)2DnWCwWji=>%RbFw@&Mvsz;^w?aoc?wQz$&NN#Sc(V(AhnGyX0J z)Vj&!oFW7Z1-*%bZv#Sc5KSle@Z_+yF*=e}NTd_~xS)&ra-)~Q#yQoE_GUEKp%Fnq zU7$L$eaF_RiTW7!EH8TI8RkLeqW#fD1__-G>LqJ#3}QV21_HSy3uN5wC+;*5_FF=F zDvTT^TTFVSct|#g+1UC2l5{gT-Abm{0F)^2OyIi`xCfvFycXc*Bp}Ur0E5yPP_w*9 z_aLvy`pPUzDQ}~cdqG-K{(b`YC2&7Lh^E|}WyK^a{YQEGu%H68IDfTt0>3E$WAi@1m~(OfQlzi_c7d}50TQI zhYI+t+8|=7z;@99$*?4VA3q*rEL8Xrq8tkV(hYLj+JEcIpC|KuiTa-zO{qs0cDCcF-<>bBQ5+-5F~CPC`jGE0Vt+_o4_v`=oZp|&ttSp{1F6g`QK~9p8xoSoYbVh zV$)7~3cBplMP*d^?+0;-@^=6=`u6~F3DfaHH`Y)(}n$O2n<&RJ=Y zP+cwIDqnmF3?$2!6Zjy&t|*K4jKKDg%|*7YC#cAM5G4FzCvm0%3f&-}V%93jYOZ(z ztt!bQ043X368O~we$7C)mKpbTfNvuB4IsRbd}{X)Ss)ATp;LhLVTX2TDcY`VWKh-X z6THyWFiUNEJqq!$-?{a4(mxXf+K{ngE;-z>bm!>=)Y=4FK5TR0=wP?x>HN@ZCW!@r z6{7?tMe{cS$}~?HBTL7gAj92vZpk?eR9MIMLWdL=5ChcAdJH=5n zlsMLhf3lHa&u|bwfzS$4JQOJDHXEekyqU~~$bnJyZGckbI{>A~GXN#%cL7T28GxI) z>^F}PH-`Ht4 zt+rR98x74n>Lq}xmH!FwMi%V@03DjHWb+#PXgEW^91Mnk5yO1qv0KR16F3$|gEP*u z_bNOK;%`&jL1dsx1qjZEfYYV{p z_-SrK zO^Z{qzVu0MahS08Fj?>Z8@k80HY;0_DlQKr0E2 zR_bJEnIRBp`k+O`mq_j<8`J?u#zvQPwX8tU6b@L9Am>PzehAlm_iDqa;VoWCrjI`% zy)OU}oIExWSX3*yI2!wOw_34wSUR@^J`ctCuJOHT*ZU^iMEcicmOa8|^>?jgn?rJ~;%-AV^v zdfYD>UfdS>Q7m2%XB$RB;E)aS#bS^zNi@@Z38tj^nE<6Z{Hdy`r|reu(?dZ~qC&4? z&2qGdi7%??Q|NG4bZ6LzzboNYS06PbT+@4nJy+ll4@v|02;k+%7)dLNd(f9tel>x= z29S?R4u{6LvRti&HdwAk^9GV&lwxstuAvU( zsQYYGul|f@hc3}uw-XL>+P*aO53o#>Z-7&Zqhz9d0Dql;Yk;_l5??1HEAX%f`Rr1x zKm$**RRcpTe;rLOyZB=CH(EGSjErL+P|NeJkua1Mcfz0o`L&pV>nVF%GjKW<))io& zWFHwG_7RP-Rc+t(LYzPZ#z=V%kCYB{LRtfoWkT-IoxY^labecONDbS9I1>ZS!1knr;ag;Ut)F&s$2V(`uiv)wyEESF9 z*~UJ#w#PL{v>r6&IvPjdn>iZoSMI7|fO^arVDAVrWw}dQCejpCR!wUjvo+C0G_gpL2b#H7 z+m>O9;ZNyh3h1ip6YY^Hs8}KnR4CsIY<}Itdsy}fHib<=8>#6qY8=)$ zxG?f_TTL1zb4iOH#p38iblS^V`V^#`*^_D}r$i(Ln(l1?YZPZ6L2F7r&`M(NSniFO z(kInU?!E4<90`8H54zgh#Q~2-R7HL}`ZZBKuUMLYGb``M97{Am&X$MJKNy>wS$pNg z2MffE@z$!`!!|8eJRX(z0ADMm8Un&bye+5d(^J_SJ`u4Sc@_*@z7UrWV086TOkD+# z6zq3fC)_dgY>i{7WZ)ItU5&mf-Zp~W)-tyF8eSgu;p!IZJ?3s8sSNu4;a-j~W)xT2 zHsIN8b4f{Zm>ix=v&@61(C2zmQgYz*n-9WJP;+*&CbeibWyUC$XPLp^j>&qId=m=^ zAG0$_$qCJZU^Mp2+q~<}VqxB97%xu}2zzKrUFD2fL%ICeH!jkt0UI?W~S|pj053~p@ei8>=wleU2K9caWvG30c&2p5_L72>~?fB+M42Wp3 z@@K*KC;+o^GPz$>pu>2%UErA9U-6Nl!dS^fp-KEg&8jw(4AN{C1P|td%&J5bBvm5C z;X5fvkF{DJM8_(* zxG>~J;WvU5pfrGRg6{3hzPNxjO)XLOqTf;(DfE*t(X6-lG8+tIQSKAxZ9?aZKCVHLh=Me0anrR*He3fHxNWt7B|PuFA*pY)59b{ z^UV#Y*IVi8}?UC2$ugyJ3LZm z_VJf7hGXW7n?YPs@u2CC5 zgmW1i{W6;#;Clp|)tn7PQ+)?07jW>T=|C)IIv)=z^g-)V$QAPeuN)_Kg4da;p!3{E zKtVcxG=U!jcy^2Z3%pKL-Y5Hi2pH|`f4dFm_V>T^Z&RB<;8+R@)=yQXJ254pK2ET` zBLYntr7uxp|2X9-tf5czn+2v3`!Bmr6}KdAbW!U{NS*v58=TBHnJxOTUbX6OfU?D> z68LF=$66h<-v%r9$U%1iqn(5P(uOk!@iR-C6bbLU`sB`tkwBjXT?zD83H)n-{Lb!P zjH7(-*DGcXgH(%t=2jP9>ONz0UL^b6=wIf;OWFlkS#)Gi^KaqE@*v?A+}-^XblACi zfwKl)YB#Zw`Tlv}bP)UkKs{3518_MBuxWQzsf&i5Yv^fqxlB* z4$pLjfyD$G{p92_f@m^)bfYP74GK^3-22BT>=*mypH?%Z?Y7vE)U*dw6)Rf#3~F&7 z7)VXtV;51OeHf(_&uFs?&+ys*5ORj0RAzWTbMTRU9>T~`UG3I$gk?mICeOv-nfjGy zqeR^{u5Zs|`z-JlllNB%GNq;fa(*V9kcMf3kUgz-@KI2CCKPLG)tPT<>zV0CBbm*K5-?Hyy2>q;CN(b<;RrfYhWR15YygH zj~Z01U~w@Cgf5xvVGOi08DtE}u5V4#W5eU4LrovNVSHm7s&)9XdyP4NkXs`L2&cktVoa-Qj3eJ#-J z^79V-%h$q{gw`;twk$`7cZfkiOo{YitGbkKn{PAjyGi~*igg$Z28oa~&}%a_fG+MK z!~tJ%s`fRnIaZ#u^3HrXk2)YE!5NuvVdYoj#|WVX&mCazP&gs(dn1$OQ)GkAN>B!#9`5 zu%hWRu0p8k*8=TAh|0kF`De>iE?RW;Psu>1LK_XJJlbKc<26tr^fcxbLf;0c5c-Zm z)qZ$^Urii}aCMP2l}D}N>lU?l_d)$CKcyu9_#X|z<5~3L$_+~zp%rM)1Z>}VRqXWm zpCZS9BnJ+5tm?(kPWuw*R#D1RAmei}L%MoN6o{Uvo(()*exGV_60M@&Hzv2o+W0M7 z*Un3EGs{1>*TKdAV2bHevu<@BntodRDCTAH?*Wv>zYmaSZ@xi>1!X_RtMe3b2$w8{ z<;?JYQSBEJq@9fvBJNq6b8h1f`yY9IjaSFE=t7X)`2^r5E@;G`ecigTq2I*+nf!l% C)loqJ diff --git a/src/builtin/obj/specialfn.olean b/src/builtin/obj/specialfn.olean index 46af94c193e2ecec15c18f9753ca33144e7beda2..18ea9a60df1cbd973e49b49b685397bad49b740d 100644 GIT binary patch delta 92 zcmZo*>t>sI^43jOGO!&kYK!8=52}H?Eu3~Bf0BQ0S>;M1& delta 81 zcmeBXYhatOkCVA5H8CeXC9`bfDMm(d2rsuZhe4S+Gp{7RBtIS`KlwRh090jSO3Gws UCKEmp1`uFXW&%;-lUteE07efNXaE2J diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp index 4c376c2f4b..2e4d9de771 100644 --- a/src/frontends/lean/parser_expr.cpp +++ b/src/frontends/lean/parser_expr.cpp @@ -260,7 +260,7 @@ expr parser_imp::get_name_ref(name const & id, pos_info const & p, bool implicit std::vector const & imp_args = get_implicit_arguments(m_env, obj->get_name()); buffer args; pos_info p = pos(); - expr f = (k == object_kind::Builtin) ? obj->get_value() : mk_constant(obj->get_name()); + expr f = mk_constant(obj->get_name()); args.push_back(save(f, p)); for (unsigned i = 0; i < imp_args.size(); i++) { if (imp_args[i]) { @@ -270,8 +270,6 @@ expr parser_imp::get_name_ref(name const & id, pos_info const & p, bool implicit } } return mk_app(args); - } else if (k == object_kind::Builtin) { - return obj->get_value(); } else { return mk_constant(obj->get_name()); } diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index f27846cb70..b210c55d1c 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -257,6 +257,15 @@ class pp_fn { return ::lean::has_implicit_arguments(m_env, n) && m_local_names.find(n) == m_local_names.end(); } + result pp_value(expr const & e) { + value const & v = to_value(e); + if (has_implicit_arguments(v.get_name())) { + return mk_result(format(get_explicit_version(m_env, v.get_name())), 1); + } else { + return mk_result(v.pp(m_unicode, m_coercion), 1); + } + } + result pp_constant(expr const & e) { name const & n = const_name(e); if (is_placeholder(e)) { @@ -267,16 +276,13 @@ class pp_fn { } else if (has_implicit_arguments(n)) { return mk_result(format(get_explicit_version(m_env, n)), 1); } else { - return mk_result(format(n), 1); - } - } - - result pp_value(expr const & e) { - value const & v = to_value(e); - if (has_implicit_arguments(v.get_name())) { - return mk_result(format(get_explicit_version(m_env, v.get_name())), 1); - } else { - return mk_result(v.pp(m_unicode, m_coercion), 1); + optional obj = m_env->find_object(const_name(e)); + if (obj && obj->is_builtin() && obj->get_name() == const_name(e)) { + // e is a constant that is referencing a builtin object. + return pp_value(obj->get_value()); + } else { + return mk_result(format(n), 1); + } } } diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index 3f33cd439d..494edf5a47 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -80,7 +80,7 @@ bool is_false(expr const & e) { // ======================================= // If-then-else builtin operator -static name g_if_name("if"); +static name g_if_name("ite"); static format g_if_fmt(g_if_name); /** \brief Semantic attachment for if-then-else operator with type @@ -108,12 +108,12 @@ public: return none_expr(); } } - virtual void write(serializer & s) const { s << "if"; } + virtual void write(serializer & s) const { s << "ite"; } }; MK_BUILTIN(if_fn, if_fn_value); MK_IS_BUILTIN(is_if_fn, mk_if_fn()); -static register_builtin_fn if_blt("if", []() { return mk_if_fn(); }); -static value::register_deserializer_fn if_ds("if", [](deserializer & ) { return mk_if_fn(); }); +static register_builtin_fn if_blt("ite", []() { return mk_if_fn(); }); +static value::register_deserializer_fn if_ds("ite", [](deserializer & ) { return mk_if_fn(); }); // ======================================= MK_CONSTANT(implies_fn, name("implies")); diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 24e6a07cdc..4d414cc803 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -1342,13 +1342,11 @@ class elaborator::imp { if (a == b) return true; if (!has_metavar(a) && !has_metavar(b)) { - if (!eq) { - if (m_type_inferer.is_convertible(a, b, ctx)) { - return true; - } else { - m_conflict = mk_failure_justification(c); - return false; - } + if (m_type_inferer.is_convertible(a, b, ctx)) { + return true; + } else { + m_conflict = mk_failure_justification(c); + return false; } } diff --git a/tests/lean/arith7.lean.expected.out b/tests/lean/arith7.lean.expected.out index 8eccc5aefc..2d1171ec3b 100644 --- a/tests/lean/arith7.lean.expected.out +++ b/tests/lean/arith7.lean.expected.out @@ -7,7 +7,7 @@ 2 ⊤ Assumed: y -if (0 ≤ -3 + y) (-3 + y) (-1 * (-3 + y)) +if (0 ≤ -3 + y) then -3 + y else -1 * (-3 + y) | x + y | > x Set: lean::pp::notation Int::gt (Int::abs (Int::add x y)) x diff --git a/tests/lean/tst1.lean b/tests/lean/tst1.lean index b872329ff7..86eb585451 100644 --- a/tests/lean/tst1.lean +++ b/tests/lean/tst1.lean @@ -1,3 +1,4 @@ +import if_then_else -- Define a "fake" type to simulate the natural numbers. This is just a test. variable N : Type variable lt : N -> N -> Bool @@ -9,7 +10,7 @@ infix 50 < : lt axiom two_lt_three : two < three definition vector (A : Type) (n : N) : Type := forall (i : N) (H : i < n), A definition const {A : Type} (n : N) (d : A) : vector A n := fun (i : N) (H : i < n), d -definition update {A : Type} {n : N} (v : vector A n) (i : N) (d : A) : vector A n := fun (j : N) (H : j < n), if (j = i) d (v j H) +definition update {A : Type} {n : N} (v : vector A n) (i : N) (d : A) : vector A n := fun (j : N) (H : j < n), if (j = i) then d else (v j H) definition select {A : Type} {n : N} (v : vector A n) (i : N) (H : i < n) : A := v i H definition map {A B C : Type} {n : N} (f : A -> B -> C) (v1 : vector A n) (v2 : vector B n) : vector C n := fun (i : N) (H : i < n), f (v1 i H) (v2 i H) print environment 10 diff --git a/tests/lean/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out index f3d47c176d..3a2e3c11f4 100644 --- a/tests/lean/tst1.lean.expected.out +++ b/tests/lean/tst1.lean.expected.out @@ -1,5 +1,6 @@ Set: pp::colors Set: pp::unicode + Imported 'if_then_else' Assumed: N Assumed: lt Assumed: zero @@ -20,12 +21,12 @@ axiom two_lt_three : two < three definition vector (A : Type) (n : N) : Type := ∀ (i : N), i < n → A definition const {A : Type} (n : N) (d : A) : vector A n := λ (i : N) (H : i < n), d definition update {A : Type} {n : N} (v : vector A n) (i : N) (d : A) : vector A n := - λ (j : N) (H : j < n), if (j = i) d (v j H) + λ (j : N) (H : j < n), if (j = i) then d else v j H definition select {A : Type} {n : N} (v : vector A n) (i : N) (H : i < n) : A := v i H definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n := λ (i : N) (H : i < n), f (v1 i H) (v2 i H) select (update (const three ⊥) two ⊤) two two_lt_three : Bool -if (two == two) ⊤ ⊥ +if (two == two) then ⊤ else ⊥ update (const three ⊥) two ⊤ : vector Bool three -------- @@ -45,4 +46,4 @@ map normal form --> f (v1 i H) (v2 i H) update normal form --> -λ (A : Type) (n : N) (v : ∀ (i : N), i < n → A) (i : N) (d : A) (j : N) (H : j < n), if (j == i) d (v j H) +λ (A : Type) (n : N) (v : ∀ (i : N), i < n → A) (i : N) (d : A) (j : N) (H : j < n), if (j == i) then d else v j H diff --git a/tests/lean/tst3.lean b/tests/lean/tst3.lean index c2bd48ba5e..c60b7acc26 100644 --- a/tests/lean/tst3.lean +++ b/tests/lean/tst3.lean @@ -1,3 +1,4 @@ +import if_then_else set_option lean::parser::verbose false. notation 10 if _ then _ : implies. print environment 1. diff --git a/tests/lean/tst3.lean.expected.out b/tests/lean/tst3.lean.expected.out index c51f19fa0a..d4f95ad91d 100644 --- a/tests/lean/tst3.lean.expected.out +++ b/tests/lean/tst3.lean.expected.out @@ -1,5 +1,12 @@ Set: pp::colors Set: pp::unicode + Imported 'if_then_else' +Notation has been redefined, the existing notation: + notation 60 if _ then _ else _ +has been replaced with: + notation 10 if _ then _ +because they conflict with each other. +The precedence of 'then' changed from 60 to 10. notation 10 if _ then _ : implies if ⊤ then ⊥ if ⊤ then (if a then ⊥)