From 770145a3613b148d5d195e896ff4ca65a8ea7bfd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 1 Jan 2014 12:40:54 -0800
Subject: [PATCH] feat(builtin): use namespaces when defining nat, int and
 real.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/int.lean            | 110 +++++++++++++++++---------------
 src/builtin/nat.lean            |  46 +++++++------
 src/builtin/obj/int.olean       | Bin 1752 -> 1664 bytes
 src/builtin/obj/kernel.olean    | Bin 21583 -> 21579 bytes
 src/builtin/obj/nat.olean       | Bin 788 -> 742 bytes
 src/builtin/obj/real.olean      | Bin 1220 -> 1139 bytes
 src/builtin/obj/specialfn.olean | Bin 1111 -> 1101 bytes
 src/builtin/real.lean           |  72 ++++++++++-----------
 src/frontends/lean/parser.cpp   |  22 ++++---
 9 files changed, 132 insertions(+), 118 deletions(-)

diff --git a/src/builtin/int.lean b/src/builtin/int.lean
index 72e81e81c7..41f43455d4 100644
--- a/src/builtin/int.lean
+++ b/src/builtin/int.lean
@@ -2,63 +2,67 @@ Import nat.
 
 Variable Int : Type.
 Alias ℤ : Int.
-
-Builtin Int::numeral.
-
-Builtin Int::add : Int → Int → Int.
-Infixl 65 + : Int::add.
-
-Builtin Int::mul : Int → Int → Int.
-Infixl 70 * : Int::mul.
-
-Builtin Int::div : Int → Int → Int.
-Infixl 70 div : Int::div.
-
-Builtin Int::le : Int → Int → Bool.
-Infix  50 <= : Int::le.
-Infix  50 ≤  : Int::le.
-
-Definition Int::ge (a b : Int) : Bool := b ≤ a.
-Infix 50 >= : Int::ge.
-Infix 50 ≥  : Int::ge.
-
-Definition Int::lt (a b : Int) : Bool := ¬ (a ≥ b).
-Infix 50 <  : Int::lt.
-
-Definition Int::gt (a b : Int) : Bool := ¬ (a ≤ b).
-Infix 50 >  : Int::gt.
-
-Definition Int::sub (a b : Int) : Int := a + -1 * b.
-Infixl 65 - : Int::sub.
-
-Definition Int::neg (a : Int) : Int := -1 * a.
-Notation 75 - _ : Int::neg.
-
-Definition Int::mod (a b : Int) : Int := a - b * (a div b).
-Infixl 70 mod : Int::mod.
-
 Builtin nat_to_int : Nat → Int.
 Coercion nat_to_int.
 
-Definition Int::divides (a b : Int) : Bool := (b mod a) = 0.
-Infix 50 | : Int::divides.
+Namespace Int.
+Builtin numeral.
 
-Definition Int::abs (a : Int) : Int := if (0 ≤ a) a (- a).
-Notation 55 | _ | : Int::abs.
+Builtin add : Int → Int → Int.
+Infixl 65 + : add.
 
-Definition Nat::sub (a b : Nat) : Int := nat_to_int a - nat_to_int b.
-Infixl 65 - : Nat::sub.
+Builtin mul : Int → Int → Int.
+Infixl 70 * : mul.
 
-Definition Nat::neg (a : Nat) : Int := - (nat_to_int a).
-Notation 75 - _ : Nat::neg.
+Builtin div : Int → Int → Int.
+Infixl 70 div : div.
 
-SetOpaque Int::sub true.
-SetOpaque Int::neg true.
-SetOpaque Int::mod true.
-SetOpaque Int::divides true.
-SetOpaque Int::abs true.
-SetOpaque Int::ge true.
-SetOpaque Int::lt true.
-SetOpaque Int::gt true.
-SetOpaque Nat::sub true.
-SetOpaque Nat::neg true.
+Builtin le : Int → Int → Bool.
+Infix  50 <= : le.
+Infix  50 ≤  : le.
+
+Definition ge (a b : Int) : Bool := b ≤ a.
+Infix 50 >= : ge.
+Infix 50 ≥  : ge.
+
+Definition lt (a b : Int) : Bool := ¬ (a ≥ b).
+Infix 50 <  : lt.
+
+Definition gt (a b : Int) : Bool := ¬ (a ≤ b).
+Infix 50 >  : gt.
+
+Definition sub (a b : Int) : Int := a + -1 * b.
+Infixl 65 - : sub.
+
+Definition neg (a : Int) : Int := -1 * a.
+Notation 75 - _ : neg.
+
+Definition mod (a b : Int) : Int := a - b * (a div b).
+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).
+Notation 55 | _ | : abs.
+
+SetOpaque sub true.
+SetOpaque neg true.
+SetOpaque mod true.
+SetOpaque divides true.
+SetOpaque abs true.
+SetOpaque ge true.
+SetOpaque lt true.
+SetOpaque gt true.
+EndNamespace.
+
+Namespace Nat.
+Definition sub (a b : Nat) : Int := nat_to_int a - nat_to_int b.
+Infixl 65 - : sub.
+
+Definition neg (a : Nat) : Int := - (nat_to_int a).
+Notation 75 - _ : neg.
+
+SetOpaque sub true.
+SetOpaque neg true.
+EndNamespace.
\ No newline at end of file
diff --git a/src/builtin/nat.lean b/src/builtin/nat.lean
index e72e34c012..e4959bd426 100644
--- a/src/builtin/nat.lean
+++ b/src/builtin/nat.lean
@@ -3,32 +3,36 @@ Import kernel.
 Variable Nat : Type.
 Alias ℕ : Nat.
 
-Builtin Nat::numeral.
+Namespace Nat.
 
-Builtin Nat::add : Nat → Nat → Nat.
-Infixl 65 +  : Nat::add.
+Builtin numeral.
 
-Builtin Nat::mul : Nat → Nat → Nat.
-Infixl 70 *  : Nat::mul.
+Builtin add : Nat → Nat → Nat.
+Infixl 65 +  : add.
 
-Builtin Nat::le  : Nat → Nat → Bool.
-Infix  50 <= : Nat::le.
-Infix  50 ≤  : Nat::le.
+Builtin mul : Nat → Nat → Nat.
+Infixl 70 *  : mul.
 
-Definition Nat::ge (a b : Nat) := b ≤ a.
-Infix 50 >= : Nat::ge.
-Infix 50 ≥  : Nat::ge.
+Builtin le  : Nat → Nat → Bool.
+Infix  50 <= : le.
+Infix  50 ≤  : le.
 
-Definition Nat::lt (a b : Nat) := ¬ (a ≥ b).
-Infix 50 <  : Nat::lt.
+Definition ge (a b : Nat) := b ≤ a.
+Infix 50 >= : ge.
+Infix 50 ≥  : ge.
 
-Definition Nat::gt (a b : Nat) := ¬ (a ≤ b).
-Infix 50 >  : Nat::gt.
+Definition lt (a b : Nat) := ¬ (a ≥ b).
+Infix 50 <  : lt.
 
-Definition Nat::id (a : Nat) := a.
-Notation 55 | _ | : Nat::id.
+Definition gt (a b : Nat) := ¬ (a ≤ b).
+Infix 50 >  : gt.
 
-SetOpaque Nat::ge true.
-SetOpaque Nat::lt true.
-SetOpaque Nat::gt true.
-SetOpaque Nat::id true.
\ No newline at end of file
+Definition id (a : Nat) := a.
+Notation 55 | _ | : id.
+
+SetOpaque ge true.
+SetOpaque lt true.
+SetOpaque gt true.
+SetOpaque id true.
+
+EndNamespace.
\ No newline at end of file
diff --git a/src/builtin/obj/int.olean b/src/builtin/obj/int.olean
index 9af0cddce7e7b4684b84af33b131617545179b26..0260a3fd6e00f93c3f6222a0b41482672ed8d8ca 100644
GIT binary patch
literal 1664
zcma)7O>fgc5FKyQBz#DGly89o3PlhU2~g7_XoFfHQq`y&kT~=b*?1Ey9J?eNPCatz
z|0sVfzl5D<C!S4nz>2Jy-M91JzMXZ_So_H!iZ$hrcQ86h$A*6DaiU|&v&1*_%^#CG
zNDNgyQbB5HFOK{Pso9@%QrYVLX%w3%p_0Y-P1=tv`eUlc-=j1ELgk3B+E9sSU(sTX
zP5XWr(ot%BlP~bpOVr-u)nx}dn#N1eCZJu0t~t;!`n?3@5!MWF#Q|F@Tm?J3<XPw&
zu3L4dW@qPO?vox+84e9KRg^z>rJ@2}OEsnT(=@i~IJ=A?gjWzg<+t_LKK$}rs!px~
zPG4G*I6M2B>BwiHgbUSTvr5T2a91-S*BQ7DAvX{<luGRJ5(M3Z7N~Ls?FhzeR4@)#
zGS(&IZKkP%@eaZUzwZ_Xcq{lig722#n@odMTWo?b_xe89Z-VdvLQs{lHH2$u#@1_a
zEScNNIuP~l3F1T#C9&jt#3Wn)QJHavSou&?9;KnIJnx^5q<G9rJJ`|_gkWonEx|*K
zRxpa(JwqnqqFq$33kmjuM4_InlF<V=Zywa|LB<Bl=xr#ae{n?g0h5Q|g#sM2;*W#9
z_pXvtak>qm!w(z{(t#Juar~?l4LG1<uvHz71vO!K_ksmVos#`k?fPxheokLbd@6In
z8h4ggq<r2YW$#2fH%tt%c9GhTg2?Q}6q&s=UiSGovgRyWT5)F2AYeW8L+*YHBQX9g
zLTtaCZC|*3VauM94c#uh-gFvzd;awT#e1eOnTZ9((iyfGl(+M{!pBY5N6>hmld#MG
GI{yHAVbzuZ

literal 1752
zcma)-O>fgc5QfK_k|LEOv<D6#g)e~;3KBwvP$^DZsUWotm5?}D4&Fo-{wRrqgw!J!
z{zv&^{Uz+YUe~jZ4@8kQv)<X~o!QxSp6D=}#fc{S^N!Ptd{NMMy~uPz*2}_zzJv=>
z$5}y}9;s<w&?t$+C8_J*SER~le-$T1oSo}}I<c9#OLhcq5JnN5<V9G-dBy>rdV$E1
z+Q7p6-i=6CNh9JpB93eXzjq^|_-7-6M_6AK!@e71vUg<-Kagi4URw%R$DMHf=W1=n
zfu2#B$6Qlag;i0yYRbvd9i{v{H+pZecNar2@4<Y;&n?DcWzPlfyNV29P0?RR5znX<
zB}JQ}9c<fnDd+){cOd8?%$`!2*=2&TZ5HN1ohxkUPz^^==dIM9q&{U-57cKcd;Gj#
z7o&~2?=THTFqf-oTdD&<ZS4ol7y$YbCU6@_5oQ<N+kXX4qtJb)Wf>>vnVw6!guY?Y
zyZ>08=Y6uB$LopZ(>#*PSDocc&U=pck=zg_kb5FI>>@^QV-&u-s|?~rt24uXeP+yU
z5EOa9Cw!di#W#DL>8x%zbI9UIFWb~kpw@Ps&k`q4JBImKDgA>jqA@g{LLP*oH_keI
z8SOT9<<e=1iY`hQP8~6_Vjme6Jn6(UHYfmg%Yof!APkSzN~Y8$ng6DVe_P#VhG+$x
z7{xb@sn|1xnSz!|B@-S>QH^t$kg``w5hYl|d#Y~B3MSZ2TYj!CCUCwo=U16k&1qD(
z&y&!Uyf~Wj^dhvk9Vh11F25BncaCtYoe@L4Gr~0&m+;JmB0O`{tyd)}T!0U==!m~&
F{{Uql5{&==

diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 82eff1ff67b6851fb23f8f644856648a7716b176..ad444dd349b5ae6d581aa37ac6149c6115b025a7 100644
GIT binary patch
delta 6121
zcmZ`-cXX7+7XRkk-L%~eNtR@5$|jq(o4RQvn@$Sp6~jX;90`*5ARxsWDT08glw2_2
zQBk@|Ri7XV2-3tS#iM|tsGvthdDs;n=$m_IKQ`gW{xRqG-MRC-ckbMoxwFSMuy;1F
zt$9o%@t;4GGIKB?siJeNBzKJ+3!e`$z;qU@)1%x#dcm-qCB@;lPHLPub@bG(iQV|c
z<a6_uN-B=bGJfmeJhQVf(8#$oE)+`TWL-FR#giZcrpfLa{2qKA(WrFdi6WlsJI~GE
zFrb%w9o;<!eeG2R>#WG=CJQ#OsD{+zx8*tu>7$4vjx1c?d2ast0lj2l?8M2V$B&1Z
z_88c$(&_BTT1r-8;iRfLDggxzBuGTqOd)bO$U+QMs9TIKl;2J&DF{asOofeVlhet+
z85<bSB8hRSn;4v8O}abpf++te&}wwX4CLr0j!c9T3A!Oo6UEY@K@&;e=`c|<jAg?P
zO)JX>t>2@p0{Z->uxilyPpfUlfp3sv3&LFlTM_Oi*oJT~!QnKceJFT~1UDf(ltlhj
z!x8^n)&wkI92)`u3>eF9gA)NwtPAXc)ocuO1&(ABV1M9rHU)+T*|`&)K@LNx6o4E!
zO-Ux69(XD!O+OQb4GAPEhEqZD0X>qpTdj4c&c^Or$%i={O0ri|(#ZGXx6~^b5%$0x
z+REg49I=1Vi1`S|6MRIh5eg;<iflNcjbwA-lD4YiQItPGijVo=;|QmdbRohS-uZLP
zwb8B$8<{jZ;69y=Er2I<9{pleSfb47tS-SfC!N0B0oc8UMlBU?`J7uTMlFEJdQZ$E
z3Kydp)=Zehhw=I1VAeiPk{jA-&wi%QOML=`JBYE*2bViImcmf*8a6vgVFgqKyUlZn
zTICG|eW+3AZTP-1LY9`n`ruoPPov}%je5ohSAum=oxDtfy<s-?6g)hrY2+&G{fQJ;
zBm9}*8ic<PT<e?RuVSA(L^kDkT5GR2IMIQ#eGbw>YK-f-Tn-|l4L<lhEDW)+UU)I2
znJ?p&kaqSQw1kdi>tJJOvvDgbme81OKKK$C!g5Kw0s6wK*cLb&Rv)_q749Tm43rn{
zL^zJ5uS2~d$I#zPC5M(8;@EcBVW>*mjp}nreUA^mNo!Do0!&PKzL@YjNEw{UcEQNO
zRi1q)Urqzx^1=PSfh$n@qzGHDND0BR1<r7my$~2)VLXUR8;Ru*!c7DZ!<cXvkIUll
zNOk}=hYvNrgPmei{|DiI(t8&IBHZi<cp}=2$5H$NiBI_8d$5*k9D~ylH<g@3@i(M#
z$_G!A$9O);7qI!36h6GR^72I`XcLTX_5nO=yu0ZPS5%2h>0=-K#0Sq_BUNFhs8mGy
zDMEjOpCb(N1_wG#F21@;Oy!*aeN(n!8HLLa6H6^(b_}fMO!g5pm`lRG#<4|2^Nk<J
z(gk?N91-=Ai19VYRn?T3;s%)k@0nffA^6j5W?zBHQk(W)WVxAGE+HI6@Oy-}5c~n*
z?aJY~*b;8)Ktfdjwq#2s{I7sr78AP&CoN+urJqnmoJl_;>>;jS5I#uoSA^nt`VHYM
zlKzfxj$&+<HJo)opEZ{K2s^ELF6j^KewH-<hj5kmyy4ip_n44e1e?vG?U9so=Q5Pp
za?H|I9JGbT|A}y`(7p{8*_^BgcG?nU=?a{;H8VfRj;zS1Mcaq^OojRf2x>6e3>(!!
z46_PTR&|*A{6!yZiwrm6m7zLD;y{G&iFq}_*~m(MuQ;L{j6qG*yx~~1s3|uX)-`HB
z8WVz$(u9Q~3?OM388DzA5RI#Yu+dWAV1yxxmH6mfZe>)ogXv&abStyM`_Z>X8d1kX
z>L!H61TDmBg{GMBTARSwSwR*m5tfl&B*I|?qY%~*j7C^bFa}|hlg`B{usNniucI6h
z>D~cqyHn2wNIdow76Iez<tzqXv^!?RBEu3QBkM~E#^X*>FT)0}3w0k!6A-Qt>33O*
z!;F+EEhz^4Fs4jJRY@c*2dtVm>eVE4P(OBygPVUsV{8z!!#`r%X2j5NBBV{ul5pfJ
zWH}k(c7iU77ZytD9po{d!s?x38Ge+oSL#AT7!)RUBU!(dgu-i7y5#c-RYN2tnTdlr
z!4qdmAAy?cBcw`m609hEn`bZojlo8JNNB*ExLC~T4RO&d5e~=I%JC9>Y&1cNBkJ~a
zRQwthSq4Hn^OzgqcO=cCs9!_@o)c>FkY&?^b5QUD!Cad5k0`)>ul_}>$XD=!!^-a+
zBH4wL)sR!kaN6OrCGu~HwvtAtkw=R!u^*Q~bbKpIgURvjS@B{GDOBW>2ZuQc79va~
zSd1`@U<q7~Z;qcU(m~WXI9ddg*@;h0nq|<Pki-h0FX3@hEfS0%aUDVBXedl{@&otI
z#0-AHEKiK#7tw2p>0I&+Ni0by@gz-iwBe{;B53!);RL;05`-jMVR4cbf|7GMMQL&i
zZ+nwHoZ@J*iyQbO*~YQa8N+dDayT?N{W%)$yqW85b5@xTP%x!ToRAtDmADrUK!_`Y
z>y){W>p_>1k6Px6=k4pRTK#CQ=$EHVC@cjhRFu-nH5aE;>hHwfcBS_m_3Bfz`7KeN
z>f|~TQY-ZnP-n6?rD0EMrh(o=l+u3p(cQwvf-0>*KM^%&iv+j=wP{I%acLyK$0#?i
zRmXF=>SUBJQ%K)ULsFa*{g@!_hS2n4{ZuaUTd$CgN{?hS;QsV_)7>b4m12GmL1h+a
z)19vEL`ECiTd3_NiP+F&NCa<}1S{PpsLP0OiZMb%bc!*8rT-XsG^14i02=*5F?u?~
z$%`UYW;(B_vN9itn}NMo$-9|8IE$b%=0v8GYhTH<8FrC#B453Jfy-@=-_G?V|3TP<
z^ml2X=3Q<(FQtyUBj9+L1~$8+IqOlk%^*f&S>x|kSg*S6UTXs;3Yl4UL;nzYtwCp2
zv*lrA=<s?ilCVUq6|m&Na6T&<r=DF9?TtED_nxWVb;p{&j6Z${rI}$`cDVi#B%G!!
zeqVN`VH%F1Ao%x)#h(LbvJ3V2yz!r_1k90>!zVg2C!Oc#f}DE8BJ6!yIc$-j8Ws%+
zhd*;7yo~68|7yXw01|Uc^h;2(NnxCl>j@UcF;gP+My`z;`7k$!8yS>W%u9pDJcq7F
z!b$L_FU|x1a9EO8VCqAzk7$vX6BM+?a6WG+D~9Pqtgt384BCf;hbzfXbCeXl=|jqW
z53IvOy6D{!K!0JdXE>u5u7qLv_(JQ<&u34-%6t=lyzIyyWqJ-(vdI1_f(ma+0otEb
zP<{iulM1YGt{~B8JJd6d-YNm~=4AL*@xtd}u?KB$^5k2d6?+IfAEX5EmRM|EZ(+UZ
zMU+2A-fSeOcr&Iji+l5FVFYY0wB5j?PYc~XZ_Gs_lD8qnUSfO62Vch9hEgzKzo1_L
zPZlLxUhsK#e1K<L;gg~c)4!47ERnrRP;srkxQM%Urq~K=i|sdX?M!i@&$Z~1JB+V$
zia@bQZ}{LYSW$w3dbK3W^2#-L0_loZYEiZmRHdyW_TZ>Ya_3DS+>0=qvYF{PmZT_D
zkva(SM$`{t-_p(s71^Y$!fx19TEY+Qi=~s3-s1X!)nsBn!dij{5sG5%5Z&H~VP08m
zlui^X<f@9RNaeyXsz`Bgs4UtNgD`NsQe|L_#e=4!x7^P5L2P*`I|_G{-;;!Iv%u+O
z?p=gb+_Pf{XOr|eSv~>s(AXJX%Spt?RivhVmitM052M+5YdPU6t+W_G1SF;SNVMgp
zc%%$m^EX}#gRpw2mAwOdhR)WVM9nwJ!Bfy!F^-qd+bb3tc2lxxJg859m+=1?MpWVz
zeP3m4+&<(Fq5@GkCiineI0m~bUHoBmp)x5Lk1Hw2rkr~*RW|k+6jdd#&tXiJn<YbE
z)$?gzpiU+E@g+i0aDOH89;+!07C}Lx`2HHYt0T+{r2f4=Pd|jGs}nfw?n)bcR_$l`
zKx8E<h>}-Hob$cI9@2e_wD*(Y?_l9D48U*07P3V!w<bl8^&MXUVFzYbMR3}aHE#Yk
z3#^To*{_gMyDFVsMv5<q0$*!EqP)D~^Dgjl6w~{gT?JMb!S{=)E|QboQfGvQx<Tv`
zM>fla8+rOWK;6qXaS};uK|8eA+DL*bl+u=w)fgx;rj4dPY_!qnh&BcrJEa6mBRiDH
zvId^2ck#F1;rbe0B84@ya@^UF$*YaNhCJs1QBrC!cxthN)iju1=;Q{~l~M=%-Z0H@
zM5K)y)#*hi`@zh{LQ?_%mbCM*SwssZ4x;VwexqAve?dUg%dvXw-AHcZi%`3TAifB-
zTM353Cr$XL^<Pc+cR*&djpN4VI(-2-q`0xJ`8K_nA4%j02y5{$12ncYc{Rx~?(hpO
zR(|6hY)J$ECL?HDSI1enF&!1xvK3(l*~JH-E>n2S|2S=(#b0f0ZE?ZuFJBlr-JG^E
t{)jr*R^omBdCv(5Ymc>>IR#@)lSWH&=e=E1rcRMqW%rn>uJN7H{{h7sy<7kQ

delta 6246
zcmZ`-33yXg7Jm07X_~evrD>X^O_ww&ZByE`=}OZb+R}|KR6sy!Wf>St>jF4~I0f;;
zL5m0n0Ua2XWfTQLMPyX4U=@L36|A6upF83*&VVb(+;eVTUvY%*<Mw~&o^$Sh&fU(<
z!Kc}gr`fhVW{_vhysdr4)H@|8WVQic<C!~Tki`F)bl8T$!z@`R&zLq%f?dq!NAEKS
zi-apIH$?8}oFz#krcRUOP6#WFh>{Xzw9`mr9)&oOU^L8>z43DA9g;Mvb5`4|8J!*2
z$>fP1t}RKiGWNk9*`_6MPIiYlQNv5-E--8I6XdpzDZjP%OeA}!Or6lF;Ve-NmT2-r
zhN6d3@{k6{G>x&DD5xia7hxlf;c^k{R4CClW#po~l~nQ&wh_!ncuOGTEyG5to_QPo
zk#e9%8?BY6-Y&t1+AK>U$~wrT2w^9|VsPtXnGdRUF*>;eb#K*;WM!~j*UTzGAMhY+
z0tmR1wSZnfyXGb|e2olmM!1XMB!s&Owj$g^@D>VSFAClu!DNK{k}04TcuSwlCc+i{
zbT$>H1x{n_a44{W&4Cz06}ug#8pgA^&|~-un-3*H4o;#i$YnB1f#`#xl*!LxSRIsZ
zT!O;-Atb4VcY+cF7fYghd9XL_VeGw`C@e#B*{>++<UirJv|KnuxELk{SEQ`qh}}vS
zk05L(xKhjr3T6ryWpF4sh5=j%u1sHz^1Dg#Q58Oh@Gm6&8^SIn{7E6^SiWMo2@T%g
zFlF{u!SWEFaV@GWQzAPZGNeB;2sD<vp1|%6<o-#)PUW~!SgnE%qtCpCl6LL-cpP>c
zZ%A8@E_RZO4JzE|;#dkt!9THig%th)rJ>$XAYU3K1@l7_*g9ArdXwcD)a)b8XH~cv
zEQ4z0b$pwK+u0^qFsPwyEB5}E6t^L~Nbq@tmk7R~hVi}F0ZVC6S!`l}!C_YR9Js@(
zE!(-397I+xsc;885N6juE{x!Ls|k9-^7u^s7}mn=>IaW!FT&G<8!fxgq=c+@tMGLg
z6rM}k^#I|O>@_$YUYGDDD*S<T-%{Z|gwsj-HjFgonEdI%8D&b29yU2yFKjneS`MQ6
zB2xdC3J<~Hh)7N;IU<c6fH4u3z9ZPVn)HsU@EA=?2?}tL$&ZQTh&Y)@&TG)ey&MLe
zd4%O1RN72lP9WSu@FcXFQ+XP?%`xmaJYybic@I0qE<J^?m-J49Hqy)bATM&X<qV2X
zlK89&&%u*i;{!MmImYraiqDhACo23D$}DEnXZ`ajf34(XhQ-T1f;E;o4PS6|4I|6*
zD*RG~7bt8zAvL(IH5$_W3Zb6hHwc6L$$&O%DxbV1)^hIus5RTPj+Q|H&WKjz=mW6W
zGTG-)Z7WH+gtkTG=KBDSr62mqYKrk&7JK${c;04b-Ei2J8tq?=PMTzF`VZZU5D`_=
z^$VA1CXmm|2qzM}g77ASzanh)9|mGSp&OYTlExH-8amcRzlg5sH_H73|BUL4v6ktQ
z3}>PyOdwhsI+1AKYv!R}MhU!!paxCoaAI173rLEM=DvZ{bVLOk89SvZ0MQBTD(r~P
zYh-#<e}XLWaMrBzA3LZhE+qdhK!Osh;*I7hf<#ap(@GR90E+B6HWq|hTghoK!fnE7
zJ3MH2v&FE(o+L8^oU=DF6J*4Uh{3`@vzPS45WYz;9H*0OEQ>K`M+l6a2XTHixcfA3
zlb#vj5rUBjkBi_Z!s(a_e)Gh~x>zVw#NMBURfComAB#p9KsGT5X&tgygn=ZDqXFaL
zYOLAlKyjGj)e)D=y^f1>F&o?y*UXaPXxz<RxWu(SGEGESOfZSOB%`1NX=_WdDWkp=
zwQmIVRj7S#gd<5U6=5|&EIPDx1k(^UxGDYfB`1R|@s&m!EiSR8rYv{3jiCbtkmnf6
zoG`^v&QjqihpWqjK9-TY41_BPdMOgTH?=FVSw+$;gpbl1W&wOW{z;2nqO346kl5E^
z<#PpEEZX&GFL}@c7p%X?;h#{G5X92qhJ?{wsl-#=JuHVSYPZwKST$*1CYVnd8-{|N
zlrg;9w6BPXxhi3=G>52hz^V|5W9e2B3f8Fft;z{Ac%yRC|4cqup5jBhgZF9=VY6SH
zJX1NAv<JwZ0!4cf=>8;{joV3MpU{B$&V&SJ7??0|=%AM~{#t=$L$9-jWxya;UNx3^
z+Aq+W6(PJp5U&jFR|HFGe!fNl9-CT<g_Tii%2Dtg!Qrsf73sMs604J&B}|xvwmOaf
z7N#%lE(}&jbhF`vE0tw0PmJOfL3Cm>uPZweTe339iH4Fw6h@+jn_xA<G=jAV(+SqW
zrNl-JNKQEBjR<Aw<UmVZqu`H2l35kNkR{f!Xfck&;|MCpM1GQ+pYD^BGWhMaA}OBV
zaxW!$xa3okL?)voFL}1J6|I(&gEkf3LQwIwz-@=_<Y;(obO_v)Y=)$i2=1vcrHQu>
zrTDm~11YH!`zRSwCI+d+hQif}OdaRnlI|T8<3HUAojh_f#pJ)U2U?3fkso2*2Tkq?
ze6TI<O55@O8^%8ZgrsJ0ouX9VH9B;3`!BsdSeBZ|6Y_FujS-(X0eMP@p+hlU!-h8V
zV7iA^7-wN`i_&|RdJSpWY$+6{xw+1av<l-~)VagIb>P*sOw$-H;kz2;e|F*@b|+j-
zD=^MO$wIO94N#e$9Dy?}1$3j1q*Ur~Z+d~T3+0a}PWPvyQzdH>6Hf02qo>%o05zXd
zoR0Iv@SAy#r_Q<%<vVCb?<1&0aoXc{_llgOM}H-Gm?Yxhpn*g>4?uc`$0XE6r;s0p
z+cF|~g?4{NsqwGq{u9Ohi3~TFU(N9FI?t1Nx3e32uMiJ>o%rEH1QnY@nQpHAW2W77
zfM|%BR~RID9f`eMU()04rVsNo_#MreUI(xDmU;`gx24`l_|O}`xuX%5OnR^4@h7jt
zKhm`^rDZux0~4Xd+LqO5T#g>bDvWn$m12}x1r~oQaTM{Y5R(aw*||nM_Vu%sS%mCN
z)4ixi%=PocEG~n->_Q_xn)Hhl@9{Y~JdQCr9=^~P<<uG1VDDPR&$%4M4-TbYFZ`?m
zXKsn{?<m=#`032``5!6%?R5Zl=GwXIleszEb#PuWuOVvkT)gef8)w~s#;0kjHWCzm
zYT;boa8?U*^P{0SKgp~tR0=~<bmr!lt534t{2AH!2nwX%DA=<q+$>H{7newQ76(RP
zV-{XkLEErlQR~Su#un(JrKp_ln_&B}iPq<^Ba2vWC8#h+E<l#;1?AUa*j^9~XA6>4
zmPX%ndNl>ovzEPt-UQqM-99^81)F@sqPD1X?zx7}i*VUjXWfZb-9!g3(ZFtnPHSNn
zr?aBadmTFO7kX7H=Av;ayU~0Pd3s%iJ^j~BV6T#;l|?D+W#}ogvR!bhXsmTFs-Gpx
zHwY>mMiv)w4vUHlufw6QxKQN~T{1cQZEkK5leS-l2L?<UK7|c9X@>qud!ZyNYEOTb
z49;t^v=6S9G<&efG-MJ(ECT%SFv4tF*UZK-|BVS%cwIfe)D~tI3rv~)gRrTzgrB+R
zOYca=m!P4F+#N$$Ll7T%hB|^L=;}TR3(FG5+C)8*j<huVzf>*;p(<y9l=o2mVHnSm
zp_R6kghiudXjdu{@*&LOa+!l2f!Oj=_C8E1zbp9^YKm9HX@uex@d3hxMCuHYIt#y+
zCv^EqW%ZM47(i-(lv^_jR1(!7C6~@e@%!BXDV=4Kpp9jyWZ3XKw8en%`0!}<9=tky
zVaUg**+T?BftnH1c}f1_h=)uEMTz4>eR}P%ccG;so?n}@D-xVX(0`Dq35kMC!~_L@
zetN3x@NUH*{m-b&3zgR^EI7$Qc0myjHU6QTYW7My`x=H-4q@LwYo(W$a!|Rc;ycu-
zAaegfC@T4j>Uz}qP%NtYO9Zhms0N!_Wxp(_vIKlafxy)fW~0>7AC#00Jyi)&ABokA
z;%j~yV*iHARriMch~DNBi=W_uk<;}}T!10XudzXRb*H>Wg3M|YtgN>3*WlLb1kV0=
zwU=XEO`<GoU}(*{E*WP(=u`9}<6AL^YE#*u#$vz=GKhXTkn!Ocbe>}Q65$1ZEdJ_K
zHM%Akic9njm=8Q`bx>a$%r3)?wf3kVt`n`SgYTLmVPoyuF-C3@97SA15ylY2CuJ~g
zQF$;rCBngR)Q9Ina2$>u9FL8I)*kcGSoEHe!(nw@Du0Id)>ZQ=E403u<F@)tUa&xY
zp8L3{?M0y`Rz(XL)9)3uvZ(Oor^Chi*(Omb>bw{-JwIg=%o|l`#doz7d_OizDIFql
zy>N7t7rt$>LR7=rgedIZOuX^^8oZStzF&j45sZaX4GtCuzck>lBWaCxj%ylgja9@*
z;jyl9l2HUm64?o%O+FS6HBAjELX((@ts6iyLcx#||CM|g_BN$MMvE3MHtldGaS9>y
z3Xt)w8<Ih6+z2y8Anh=?$^;)acd#^Q80`#|L(~l8!8y8&KLz)WF7dx%{Vz!_kAf}H
MdRZO<nJrQO1KTRCg#Z8m

diff --git a/src/builtin/obj/nat.olean b/src/builtin/obj/nat.olean
index 445ede6f4cf12ec2057328353c935e54c73d43dd..81772f9907cbd6a3000453f4020d7a4600e08f10 100644
GIT binary patch
literal 742
zcmZuvu};G<5IwtT0}RlLA{e?AF~EXYSW2Z<P>H1sNUX?J+{(hWtKe>oEd2of0DdfA
zg6|p>yCjONcfNP`-r2TV3Nu$)Liw@B<;vy`-ehj1h8K|op9%*l13t43Mp}t?;Kk<`
z@NLO>t+Z3-SvqJK&%B0mhr(BpWiYi)IAskMFn&dqBMcf5b-C6%)JvjHkeWnPZ#Zr`
zxC7={H%M*9sbcdT<nHAh5*leCp~c1D7%e`-TEE4|)@t7cqkY;UctG$R*Ct9)PZmoJ
zOBZxBdpj13&Ck|HnI$LKDAlgcNr!TzeT1+>uuZVfx$(CFWT%aG7<r2A3<AAFsPq=K
zdOhr%l1LX}kKhTxKCazr_&T*=pmrRnsVtlh8(mQ6GlKtYbN&JTPkr{5PU;k%Rss@a
Yr~b}Z75Q@uB0p6Sc~$mcvI)NJUk|EjApigX

literal 788
zcmZvbu}T9$5Qb+*O)yr90Skpdv`HGVv5A2M4cNp&u$2wB35T2AaBezF8y~<oFfW!T
zab|LIx85DcGP67XeE-~X-Wu)ZsWp&4>T$X9S%5c_Ib-2PXMj^3ps4_7KETMP`W<ll
z`3<;}jMu3Rse3j7_8e7SL%t*Ft4<P_`k+JV9SaopMLEKKY0T%bV!5{e6g^Q)as{8q
z3bG#~26v!{b(1T2ytrWd^;4<1H*?r|S{P`c{u{7?Gnur7IQE{{2b>=B(vt8*!b@Hc
z87rMt3>?Oeh){8~i5zi7;mC$MM{R~3iHCCz+Y(+#*hO@7Um&(l*_IM-v8_SGBua_7
zsAYDz`;IBCJHou;-A<R+v*JV45r+|x7$stwl&9ooJ?Y+;uwoza1L$qi>1}?~)B&DW
Xy0}MGWHenVBXTJtoqBM|g#UzJ7zl&y

diff --git a/src/builtin/obj/real.olean b/src/builtin/obj/real.olean
index a8a66e42dd640972b9b51ea83f6c3a47d39583de..1054b819fd0d2b61ff7f36e84237beb3f52ff06b 100644
GIT binary patch
literal 1139
zcma)+Pfy!G5XHx13J011r4p?YMATFWQKA0f&<mvsZ4;qN9E#Lyv}rbx)nykso1S{)
z!iV72ezAO#dY+wR9a4!X+Kjz#=J))xjx$=>L1Hu&pXmJR+NGX;>eOmO#g$clS|--h
zca;)<)5_3VMBH<pS|(8=;>pb&aX#s6oEV>2inE5UcimLvpPWvAB+f#@pY?z^8$H`z
zWkt*v8EiV`ktkPWiJP)=GcFp$M<lmqGXajN0AFfPF`#dzxAN<*>i6lwdF2Zu5x)Yi
zCDST1-_qN?8k+^}A+&ALR?FIc@@ql+dam6lYqP-17EV6kY2L})&GOdd_D`@Up{?ZM
z4>ch%>7lIb;dhJq%sE4Z>?(3^3uP7MOIbIOoGek9bz0a!mX8-aPHz9^Mv7fnk#XzB
zFLP3dZX-9cEy6mCJVn`Lw%N%c7^=YwT$K%-1jHvaCk~eq4?^NI!5o1293@UrV;(@X
zgm)V7b^_jL+*|gD#{d>t*M)Kn;4Vs_DtI)M)%-vny#-_;-J|>vVqh&GTRjZPA+RBo
zj}I9w!mnuE3r4Hn=zpV;RcAj=2GUBMJhkZyh2XG2*S;4d^KZ(&Ygy}iU|-M|+i%Ms
F%|9>ur%V6<

literal 1220
zcma)+!A=4(5Qb+9!a<G-2M?O8QKJFW#F!`&K_xLJU^MYciWIVOY0XkRdGz8#c+(f-
zN$kw-!gj$#LYgVe-|z3VQ{@XT2c9n=`Z%|vR~2Y@5rGswL^H{C9C}j26Ayqr2<}7P
z0oGF*8otNJz@{Hxz`~W96VKP4d=wfo0j3^8^iw$R@_rxMN^|Wgi4un$kha0H;o6vx
z(u^j4O0!RzR;<B<l&0^!r8HGrg9#~(sfTT?b^(s@cpP)EV0Omz^LsJnS_~lC%}_v&
z@whrU)}t~N7;7qJJg?w%4Tl1S>lAL|xQb+2+p&@LlqrK)F!f`b!jyz5UoSINq9ZJZ
zo;DF)B2QZsx{OJ4;y~Vt=*=O6wzrziHJ~JSxRmQAxw{B+iMvOki{r+;BFm_Cn`$sg
z>Uh#yw%tl}V~JHkN`=BIg#^sfHYv=7x4C>os8qen_6<g0(ts4hq=6*&1Yu|YAz<QN
zd=GKOB!TzFe-X}6*xbo@0}P-URx<9**&PF_b7SF18G8rw%^T@yOh?+hbIi-o)v8O)
zex*e495ps{@WwIohRpt^PGD{Gs>BUJ6>p%idos{*Gm!uv9C9;Tlj?Q}H?rTtm+Kb@
C56(FN

diff --git a/src/builtin/obj/specialfn.olean b/src/builtin/obj/specialfn.olean
index 2f41ac615530eb94607c00f7cc202f9ddb8bf547..3ffd8197c6f8fede317fc3cb27a9e64955079c99 100644
GIT binary patch
delta 231
zcmcc4ah7AkOHSsZ)Wn?ll+3b;Uu_uqCmS(3G73#DVRU2@VE_W|$@(mkldmu;vx$MY
z9AK^(lM186WNRjMsOH?#oXL4iR;&;W>zLHVr9n&y6%Z+)0<j@6C52(~K}O-pOw4f#
zvPkmEOdyUp10#rnaHJ+TFe@v_g9M<4K*f<2iBCSvtjwr5S&K!EQED<9i!!4!h|Lc*
N$u%#<Ei)&T0RRh%CdU8(

delta 218
zcmX@hah+qrOCBZ`rl8cs9EOz4GKPttY#0S6>oYnsicBs9l46rL14)U=Um2Ykr6yZ2
zsl!$0mgX=_&S0`)gJ_<-oJn0$fdL34R6wMF3e4EVloW=^Pne1nz~WF@WhRg!Nd`s`
z1>wj~E@M_!Py-2|D3V83BsqB}vofQ`WCa#EM)}EqfNU)gn;&YDYhH?5W=<*t0C~42
Ad;kCd

diff --git a/src/builtin/real.lean b/src/builtin/real.lean
index 700fde5393..2fcc1b83fe 100644
--- a/src/builtin/real.lean
+++ b/src/builtin/real.lean
@@ -2,43 +2,43 @@ Import int.
 
 Variable Real : Type.
 Alias ℝ : Real.
-
-Builtin Real::numeral.
-
-Builtin Real::add : Real → Real → Real.
-Infixl 65 + : Real::add.
-
-Builtin Real::mul : Real → Real → Real.
-Infixl 70 * : Real::mul.
-
-Builtin Real::div : Real → Real → Real.
-Infixl 70 / : Real::div.
-
-Builtin Real::le : Real → Real → Bool.
-Infix  50 <= : Real::le.
-Infix  50 ≤  : Real::le.
-
-Definition Real::ge (a b : Real) : Bool := b ≤ a.
-Infix 50 >= : Real::ge.
-Infix 50 ≥  : Real::ge.
-
-Definition Real::lt (a b : Real) : Bool := ¬ (a ≥ b).
-Infix 50 <  : Real::lt.
-
-Definition Real::gt (a b : Real) : Bool := ¬ (a ≤ b).
-Infix 50 >  : Real::gt.
-
-Definition Real::sub (a b : Real) : Real := a + -1.0 * b.
-Infixl 65 - : Real::sub.
-
-Definition Real::neg (a : Real) : Real := -1.0 * a.
-Notation 75 - _ : Real::neg.
-
-Definition Real::abs (a : Real) : Real := if (0.0 ≤ a) a (- a).
-Notation 55 | _ | : Real::abs.
-
 Builtin int_to_real : Int → Real.
 Coercion int_to_real.
-
 Definition nat_to_real (a : Nat) : Real := int_to_real (nat_to_int a).
 Coercion nat_to_real.
+
+Namespace Real.
+Builtin numeral.
+
+Builtin add : Real → Real → Real.
+Infixl 65 + : add.
+
+Builtin mul : Real → Real → Real.
+Infixl 70 * : mul.
+
+Builtin div : Real → Real → Real.
+Infixl 70 / : div.
+
+Builtin le : Real → Real → Bool.
+Infix  50 <= : le.
+Infix  50 ≤  : le.
+
+Definition ge (a b : Real) : Bool := b ≤ a.
+Infix 50 >= : ge.
+Infix 50 ≥  : ge.
+
+Definition lt (a b : Real) : Bool := ¬ (a ≥ b).
+Infix 50 <  : lt.
+
+Definition gt (a b : Real) : Bool := ¬ (a ≤ b).
+Infix 50 >  : gt.
+
+Definition sub (a b : Real) : Real := a + -1.0 * b.
+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).
+Notation 55 | _ | : abs.
+EndNamespace.
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 50e7cd372b..8f5ac400f9 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -914,8 +914,11 @@ class parser::imp {
        \brief Try to find an object (Definition or Postulate) named \c
        id in the frontend/environment. If there isn't one, then tries
        to check if \c id is a builtin symbol. If it is not throws an error.
+
+       If \c implicit_args is true, then we also parse explicit arguments until
+       we have a placeholder forall implicit ones.
     */
-    expr get_name_ref(name const & id, pos_info const & p) {
+    expr get_name_ref(name const & id, pos_info const & p, bool implicit_args = true) {
         lean_assert(!m_namespace_prefixes.empty());
         auto it    = m_namespace_prefixes.end();
         auto begin = m_namespace_prefixes.begin();
@@ -926,7 +929,7 @@ class parser::imp {
             if (obj) {
                 object_kind k      = obj->kind();
                 if (k == object_kind::Definition || k == object_kind::Postulate || k == object_kind::Builtin) {
-                    if (has_implicit_arguments(m_env, obj->get_name())) {
+                    if (implicit_args && has_implicit_arguments(m_env, obj->get_name())) {
                         std::vector<bool> const & imp_args = get_implicit_arguments(m_env, obj->get_name());
                         buffer<expr> args;
                         pos_info p = pos();
@@ -2278,8 +2281,9 @@ class parser::imp {
         unsigned prec = parse_precedence();
         name op_id = parse_op_id();
         check_colon_next("invalid operator definition, ':' expected");
+        auto name_pos = pos();
         name name_id = check_identifier_next("invalid operator definition, identifier expected");
-        expr d     = mk_constant(name_id);
+        expr d       = get_name_ref(name_id, name_pos, false);
         switch (fx) {
         case fixity::Infix:   add_infix(m_env, m_io_state, op_id, prec, d); break;
         case fixity::Infixl:  add_infixl(m_env, m_io_state, op_id, prec, d); break;
@@ -2319,8 +2323,9 @@ class parser::imp {
                     if (parts.size() == 0) {
                         throw parser_error("invalid notation declaration, it must have at least one identifier", p);
                     }
+                    auto id_pos = pos();
                     name name_id = check_identifier_next("invalid notation declaration, identifier expected");
-                    expr d     = mk_constant(name_id);
+                    expr d       = get_name_ref(name_id, id_pos, false);
                     if (parts.size() == 1) {
                         if (first_placeholder && prev_placeholder) {
                             // infix: _ ID _
@@ -2593,9 +2598,10 @@ class parser::imp {
         next();
         auto id_pos = pos();
         name id = check_identifier_next("invalid builtin declaration, identifier expected");
-        auto d  = get_builtin(id);
+        name full_id = mk_full_name(id);
+        auto d  = get_builtin(full_id);
         if (!d)
-            throw parser_error(sstream() << "unknown builtin '" << id << "'", id_pos);
+            throw parser_error(sstream() << "unknown builtin '" << full_id << "'", id_pos);
         expr b = d->first;
         if (d->second) {
             m_env->add_builtin_set(b);
@@ -2623,8 +2629,8 @@ class parser::imp {
         }
         m_env->add_builtin(d->first);
         if (m_verbose)
-            regular(m_io_state) << "  Added: " << id << endl;
-        register_implicit_arguments(id, bindings);
+            regular(m_io_state) << "  Added: " << full_id << endl;
+        register_implicit_arguments(full_id, bindings);
     }
 
     void parse_namespace() {