From 097b10e424cded07fe4f879f0a55dfae96b9392d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 29 Dec 2013 21:59:57 -0800
Subject: [PATCH] refactor(kernel/builtin): move builtin declarations to basic

There is a lot to be done. We should do the same for Nat, Int and Real.
We also should cleanup the file builtin.cpp and builtin.h.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/basic.lean          |   9 +++++++
 src/builtin/basic.olean         | Bin 19907 -> 20029 bytes
 src/frontends/lean/frontend.cpp |   4 +--
 src/frontends/lean/notation.cpp |   2 +-
 src/frontends/lean/parser.cpp   |  44 +++++++++++++++++++++++++++++++-
 src/kernel/builtin.cpp          |  16 +++---------
 src/kernel/builtin.h            |   4 ---
 src/kernel/environment.cpp      |  27 +++++++++++++++++++-
 src/kernel/environment.h        |  18 +++++++++++++
 src/library/all/all.cpp         |   1 -
 10 files changed, 101 insertions(+), 24 deletions(-)

diff --git a/src/builtin/basic.lean b/src/builtin/basic.lean
index 28ca3f742..ca95b1bb8 100644
--- a/src/builtin/basic.lean
+++ b/src/builtin/basic.lean
@@ -1,5 +1,14 @@
 Import macros
 
+Universe M : 512.
+Universe U : M+512.
+
+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)
 Definition TypeM := (Type M)
 
diff --git a/src/builtin/basic.olean b/src/builtin/basic.olean
index 9f1b6434fb932dea677e393e895c0564d52e87ce..41d411e4424e9e0bb3e691a446fd490f51a027ac 100644
GIT binary patch
literal 20029
zcmcIs36NdIb$##sW&X?%n?i;v>{!Gl4aV3k8ce`!Vk8EnARz;Tpu!SH(nuOJnvrHk
zVvz_CyI86qF*2JS9Ag0?0n8FRLSTVo3=)eGK|o}aV1jHS5n~+8;z}?f_ng!Hy8rwC
z3y~^M)wJ&GzI~T-Z!fR=jYftB`iB<|4h<ykCp~3&aK*sr*g%raPSP|<vLsEic_ZUV
zXgDQrV5hnLqe(VxWMn95Gk*I?r!5~G8Xp`^O5>x;2a^10VgHcH%^wFBCNq~TO)~oz
zozi0l7A9HW`AY{*F+q^T!YpV*dnIq4?VC}p#*B@FOO_4|4vZz$tl!MGpOTUDKqNKy
zT;T%?lI<k-Mp;799_h8m^n{V|{_(+)VYH>$kw=kh&n)w*l6r=%m#uE#kZB7SHZyBN
zY}QAiWCG3Fm1Hd#Q?KTT$Pg3UV8k`K5oo0W!xq5^mssx}P&P4Ou$Q7}mE<a5@bH~r
zPxi?&h?MY=(O9;}yen4nadhgUbDtnN8Rc%1P)=^;=c-k7WMY<?hJu%89MHOL>*aqJ
zHxhvU;RVf%?2e73HQh9l=5@<FnMxyry#;gj-kTaHWf>F|8V@*Q2aQ`Vzpbv7)-D_w
z?H?L4gL@Q&ijiNW{S1yXI=20DK=NqXz8}cx%$}r@oo55sk{5LvVgu(5j*VlK?6mAD
z=scUUyFq@@;X?hNmHb?h+9pvcwbG%1W%UaCWf5|PoUto^3>{}v-60_RNgfJvUNj~!
zdEn<@`%Md3dL*TGXPN1B1K`70a0KKIQ|*x;M@Sw8a;f}lV#nduTC`*96*qZHhG9z2
zc{Z;qkj`U2S}v?+Go~a_su4S@?52PWkC}J52M=iqX~ztX&0pL<x@dseQ4o5W_0O|L
zb865)k*ODXY!ErU-==AwZ%$$^*o<UsjosX(eTp@nvuKK8ZHZpM&XWcf7V_Dpfbx`l
z-j)*~n%<qfeBKx)t|(QDnd1#5K#gXynr2cF4a#U6{V#c)eWtUV+7Hu}dJ(7JpJJxe
znLuql$+JK{Nb=7>K1A|tkUu0jkD2!{Dt^R@`5-s$L!bMYB^7vEMp5$Pu@c1r4O&#a
z*Jps$oJNFt$NTFYo@S2@ZR)@zgk{XlC=@JlHLp#`suJ3`!sFio`*j&>x_gGl2glA|
zLiu^f=7BHyt;MRvI0&gr1z8kO@6S+B)6<YSJMT|5Ta;8`%?dc-(#5E>Qv*r}lxiW5
zG$<Sz>_o7=T{iTUT>yH<$>%SD?@?||v-TvN<ngv~<>p1`i{_d@=5xUXb)x%5`-cm2
zyJSzPX49#}2nE#!tCScqpXp<SVNV^J9PGI}er6N%D_4K939Vw>q-oz`+rNztt{Ch`
z7|fr^jO~d@rtP6B#kG9kgn?tZADl#{-IE%-pvYKrMFP&=*>RFE1Ew&sG!2vFV7SUU
zrnC2E*W<bDLDa<NJ)8pf4~0M(4eA{lEF|U(NV4p;BBidcf;x-j)od!NT}_d(cy@*k
zOUvb>g{_Ez&JKh-I3^)fa}6|}L-JaXLnN;gFDjPEgdW9_MzK5f`Yik!I2oqiWldM1
zbY;i@<uXlz5W1gH?F|sKlH}I|`3;bN&f32Qd6A!($N~{1$|1*syi%UmnR&f6+FSv&
zju}}#Z^%-`hNERI0WBppxgCI#3<~}x1Ycc@$HW$0TI4~lwOKASRj$0a3CeGw9p8@G
zP<^Xxx;}|E+7U?rjL+@4>!|cDjgcGar{dy6`Yp&NRI~eHjNG;&UB`eHW=><YaUJkW
z16iW=H$&<=lD7o%R*6By{U{zF!{4eiD%N*p(SC&1maIO>DmIIOVWZv&zNV%)Wy@%O
zoC$(Lo_Z(OScOZ7=_AAAqy0-qn!V+vTg<P9EtHH79!Ab8oo|P_E%fD%K;9Xg{RwJ+
z+J$mMB&QHP<`Rq4+?`_FN&1RhTqA#T@9IPN_r~eG)8x>Yb@P1cGn&kmLI|Vbc{en_
zNq_DE`4-80LB37$A40_5(G>kxG%%}+4z(~AJ`8t31ar+^N3C*7lZ4AU5CbU?f<X=_
zLH<2Z9W>@21GzTthU!ifyU4_E$;9?-Z1Kps`wg78baY^B3~%Nxo*^(<mvxIHrO5c8
zWS{VE2KzKKHIZFpk!U#LCNm5qSUE|NzKd3B2S)6I_f4e7{sx($3nh5;zY8@n{N2sq
zpV}J!fRJXZ2O)4OgYZxwe-Imm>Z4Kg1jlI<Ml@4AJO1~9=E(tr{|9UyvGuTAh}pF9
zrDkv~Dhw#<WzeUBj8?2iA#4%R+7QT%AQ!XtF_448DN37wdY*>Hm}KJ~w_HzJHy?(6
zG(y?$J$nQaf@jNz=Z`lXjF%!Cf;*abpisl`Nl=&4`X2}KDRn@_WhgF}rQekag;@{6
z+?qwwTlfU3>n&`WuQ#-^P&xWE#N0p&|2dG)1PieN$-WU!5vj~w-(W5{*I3ca+)b#K
zx%NW+r2?2UD9iFEpNDAxH=>+)6I%EzgxpE;IgsBW`8>$Gx~#05lZaM6iq^){2LsMn
zNw~*!Gh}F6WHtiM+@5H61VAA?4K_*^t-)HB>GkoaARl4v3m_jY+UUCZk^U5=dSkXg
z1&!$$9UVEhZ^Rl}oW5qy!zTaQL8&rsH%O$9iuQ|me4ZBlERZjO{E3W<I(V~Qnnb%$
z<Zqk*hAy)1q=B)Kp%nv#h|U9d_Nv+C-ZdFZnr4R9ZH}Uq_2=wF`+gC~R|GUF{u9M7
z$?zW<z^M3@AJ~PlQ?kY=83jb0A6vl?LXLx(W*eW9y)Vv(Fc5VfNhUq=_-jtHs)O>7
zuu27O-%e2^UkxOjD=ARF%v~;FRx4@O_!`JIc6%LUM?5S`T~-y30C{gC!0MCI9`STo
zZZhcum$E|LqO~HJw=(;y;OB8jsR_Gc1D2{fX@|y6Wm$q0N=jfX@qC&{Y93&SLg7cm
zHt@RFU_0$vK3+JI(+~)%p&-uwx6%Jd!uL)UZNC*Ss(JL7>5XcehIeQ@4z{FvN4OFl
zOUH3yVKwdKW6<ng%-ya}ppwtK@)iVga5o-RG@ie;I-#H|@4}wbN&XJx86@8Wc_zvK
z1$nlAS%ewPL}e~H7O;|M4|KhxygE@2XjE{#_5VW|vcJiBNTUNE{`3QO5wQ~AgE?`O
zR<V`?;zE)o7{XWLv<&hR)}knVC3aYON=ML`(BTRlW|IO=ecs3Sjg7~ZJS17x*Z9uh
zq5^pqOBB?O%e2x>Bx@koXaL}y+w-XgC?@G~R+MfdN&WCHxx!DhDe_c6_b%(3X|HA@
zoK(n#+c&pz(iQfX5gpd8bT^H_9=~*tR1V2et4Y!>6dPzapZ!u<y3d&)2DZsNw-tBJ
zI-pYA@X12k11=iHI#74+=BGtX#I27w{gGfg0ouZmVCgY0p#*p7sd87RgG}a>V=Sa}
zio3qj!vtVgkdKnwjc`st1z$8v8$mwCwvUCjCoz&s*s-~`-9bK0HeBYFHY>T#Fkf|2
zsYBq9OB!L7Y_V}CrB`Js-&*7t<B<7bM&sEkKbY3<Fq|IckC>c19SJnHCm#T`24a5J
zX{V3jbh$*Ow3BJnfUAZaxkz$Hn|>U2a5YMC%~-Ayluv@>!jw(~S!3;9MD&kP(GEn*
z$jWjj+dc(yR}UjxjmM~=iuO-M=f7H-G!Hf6CT}37ynh{Td!ovpof5YXhAn`kaL|40
zrX%ZgA1Da<S?-DQQ|G;9OH_BvOMr3gTYt<;SmiNEr3R6~%3nU5WEaSzNPe1F?t_Y{
z#PVp6J#70-Xgh{&y`gPikTb~kS&%bHeh%a;lDNw(&)Jt_{$d@nbCnjNB;{*FqGNeL
zK7d>-A3&bNkfwVw!L?Q4WZOm-_x%ETvtJ%}yY9A%^dmd!MrL$d#sHx3muozts3Odo
ziH_y%uA8!>LDG1`iz!9v<gQsE)?%%p<D$$uqICfDUrq8rkk^pxX3VZd#dRpIXYD~C
zzfR#cjnjXnZ|ti!c7zC{p36b`X7o=EfLc^)!X-4h!~0vc+qlYEzczfJw|>fsb2~;L
znnVvaCFSqY8C)5c?<09A)9nkWSjTj`ALIiX%kRh6I#!=*??i{rfkR>7B)<-BGW}A&
zE>giE<c8?AD4s&`xVDZ1MknPb*qzWZd9ad}AOAE(EhERqW*ijsH15;DzftjNkK@Bo
zL3{Z{KmC5*o*dl0yxrfq+?u9Ej|;WE2hp?x8AzebdBG<empAGzK{?q-Y34lw25pB&
z>5(A$7L-l}`5J4FW)}Vm6?i)+6W+9kU`|8D8ziSQX1_tjn<(CvS#Qa#N_LVvT(q`I
z$-gvE^n);~LQFqTa&LQ9hVDhXwf>=!p6Z|=1$IdVx+}X>Y+&(8p<W}{!@61SvQ~SE
zp?DPdsZ4M$F_k?gqmH0xQpO`Ge_fX1BLV-Cpiu4P$jBE<J6+Ai*2Ro^6%4#nRrV$9
zGePc0@_3N@lbi*VE0``S2g;|(S>`@EQDj{PR*nE?GMPH50gpV<=lNe{nvX%?Q1TGM
zbbm@KQ|SrTu`)A~S4PEA#1Taf5{8PU^PHvqcB1Bv72K13&?E|9ABnPWgGAuV8&S>^
zzQN2Hoj$_rRug7&Eg{_9NaeH|@+OI1{lhcO)@Joo<EflR4^AWLH>-F!9mQFKFg*K&
zI9;=j-q-|7P@%-2_kMF*Ss*mGC<X+@Gw__bG9ZS{WS~T`1`E!j8Qy}kVhf}(SRjkM
z0>$%!*a9*r>LySYtc)#C8|}o4$ehuhv9Xc)T%ZbIuXaZimDLXQre;Kyfz()H0M3SU
zt4a0;avn(^7Ih5WBQK-MKuWv-+(BRHxWmJGkB2pgAr#UTRR%ILgW(P>>ggo{%rc5n
z;3x+&sIg1#8JZQ`k%f{%vsLIIS;ni)pPMtc=vbJ!FAk`z_}GGe7B%>(JZHW2j_eLs
z<KDp_X9i9Nlgi6<fg)mPQIQ4XguR|aZ9P;J_eKm)giH*05D;u~x#N*?-fwR3K61QD
zJfO8oEOplrgiB?eJ&{*|FTlzk2v=PQVk4+1#;^K^kQr7U`<};zz}?chDI%zo2m-F5
zIJ536gJ`bfjG=-fX&9~^;)f3&4nuLc;ufCG1beX7*mnXP3V6whq<S<>u}4lD)gC?u
zkyr?;hk22Qd;Gzrn30kvCoLY+w<6e!xOpY^2Ua<Z(S6*CYG3Tn+=BAC;5gkYpIhgT
zHA$Gv$o)B!GQ2;Q#5Ba6p%vs~RjAJO@=tGcj!NX*tk%xurbNNI0HQ}_F%E%j3#%Lm
z%=vTm{HPM<rf}Tcv)}6ZJTOehP*Gi#+tP<mwi|H<mjEHfyjg{wU(R=^*fF@^<Q7D+
zOcW4oLXzs0WV}NBSFq};Jk~8tAjV)Np|$xU2)nik8iBcJ3nj?txe~=1p|MgmGNs4%
z7(Gp}ploepf*K-n3Cy|8BO=WaH(KwG&S|T6Ls8H0f)+cJ>RM$v?;?dhW%8Mp3WYC2
z@LF2%6_Ro8<MpSyJ`6lP``o-=tdB?<Y<2U?Ce~=KqYFynCmO1)OS*wNP~7hYua5;w
zj3h`fz0sJB1xM8mnr5?D@SoQ3_AR{}>VFY?z6~|ogXeno25xK6D})38cJ$xo`M1Xo
zkyZQz#~Isd_fvh(?S887xrl~1Mi57pfs_^o7l-@R_efq9$iE~RIo^iB)z+3f;+~x&
zZCUJymQn&52T5VpGU{=XNf3<_%C?WeaT(_Yq8cZgZM(*yZY2e$a%~fX6yGPfUR=h5
zM{Vefh1vc!SG@sEyZT0OVrgpY_8viZ0|1O?%n{?F<aK=@3l}qO%13WM1njU6jBcAr
zJuYu-foneLNwV=fq#66w=zpr*8q!Xt$S0%%9FV}V(ss57ZC>mnjZrYwl@-PQzU!ce
z6kJhPH>o?PY+-BR6pc|okaX%gBifcX&g3{jaL&sd@L}cgl~9`g1uEp=D$V3qqoVDi
z0C0;PL_m(#>;3r#^u4qN!r~K5;KNYNKXGfjDoz9X$XrNrey(|KS2--hJ|ch}^$Jk7
zGM~!XLuOc+-e^VJH(OvSa{`t(vmXmBT*4Aww%sf&uUC+rF)fxw0a;iU1?S&D)_0n~
zS>(<^YFkHxe8R00sQPX&txMb>!lf_6;}#h;Li+=RD3`AwtlLo#ih|+2efP$ccAt~N
zMg@yX^~JLBC{_^@o6~wGTlV9<g*%jJd%<;!(t#@YJS8$JkQzX@z|9vbFzHs3!aIBm
z-Q6IW#=GxCB5{FCgA8sZlX@AZ#*adf&N|ix8GeuFyr(lCEH=v0NNl!av5?I(AB(}9
z(I)8DCd3#N4}N%a;r<#eQbb5^H_<izab9`{$>0J{YLl)8$q~Ad<oL7OAVcWZ%OH*+
z_D%+CBkLTjJ3_ZnY=mwk_CuiCyQ~?yvm6Gx?xpFjhLK?f(ZqMDHC^!BOEMrKH2nwL
zlq4V{Nva5agx=L&djQVWgo>R&t4@r7io~d*i5Pn5<_H|iN3T$BXxA=rayXRv?USag
zXsAblB~Z9qs9i$xK9a#{0aa^|8K)f)4>B8ubA9gslPuzM=)E%oxlv%8Y7qD#lFZ+S
z=I{I-$hEi@Yo270c)c5~H=Q-T8$B4vhd|!X71AyP@iP%1Cksegp^G6JuX%fS;+lW>
z@O|T{yWr|w77p^UJGCo?CV#P6%}(SERQfRU#n@__;EccZ%Azaf_?(|_4VA;u$xeb8
z`r5xv;v-{>fEAiwX0zaD0{s)T{g~trLF$8nAAx*^wU6)u=228^W?I#r1^paSp!P2)
zws^$AneZyR1Zo=kCku+TR>vE|+Dk^&UeTK`?s=2i8~!3pE}?D#Nl?@5*Y%-y{+jCt
zR$qU4@*z=w65{aNZqeBp)a?&Q_1CiO<)Lq%P=LOjqd9Nhvk3j;P^r%no&c%O67U5_
zyS_zuiqLODMLVHy$Hxfmoq)dm4^Vuh4*G*~tmZ_}N43@^Jx)zzjSMc<Dn%3=+!`nC
zpV?7x=70lddhNUd%}2yzR^@|(Jy7@y=GMa@n!J>~_NNm}?)I59ILwbiIB#};fgCZx
zs}%X#-b?a1kTcq|S@yS8t=0S~0JhsLmCOzle5op^oZraAW#B~c>kzKcW2m8rnPY#>
z+hC5p$ja;SC~?#|4D6g~r4vg#qYm5_r{AaTLQ}i%4aV4hsThr{y(pQiB~%;5U}YT=
z@UHfAE;uPho(T!5Q~dNmqu0&8k>76qasIhiD)(tw3qPRg+e$~g$k;>On@kZG4XYQy
zcn6&<fn3p??PqAaw?Q$xTo}3}eH=7&mv_nh5VQ`R67wW4{I*kfx;CHpBs-P%g_PMu
z4?@}(M#b~aa;Oy(1Nbt$;`avWR*+9Mq<uk6{LOR>M##2&q`B{yW4q$C5118Hyb<-N
zOZ(8nC#g%0|Bjqf+5~fa@^|<Q0|N2Hbz@!HOJWD7Pj`1M<|dgG>}eTwC{w(hiT0dK
z4%R6Jx05Y$LS2e%uUX%YePT9L@UloD#U}EU;e{hZ3zSTSPZpbfBouud0CfsQj@e-h
zMS#>^)N=Uv_9uS7e05BRjAUvT%2nXhg&6y=ryOJI{o0y44kr0uAP*(^8<1Zh`KAm)
z#bK;?izNK-z#UM>5nOES!wA9`SWcBHvd|!$-E~Y0;--@qUrpCrjEZAW^rAQx#h*a7
zT}_?qmvOtJiab$PY~vYCvIM-mOk+6Q$nS!HCHC8~5XB-Ci)9uC>9SA8Q9v+mglrL<
zSnE4_!KJST!P+rXGv1ZX2vkLy?4ZK_`v@6PuurEUo1;%v%JN75C4jz*qcZ5xJYA*D
zY$76I!ci(z-GbEd)uQeCM2;pzGR(Z;0hz~yiQtoYx-hPEqoX!IZ<A~g55EbGK3OGH
z+6z!-S<BIJ@T6l6irXP4Khh>bG$HbvhO)cH0D9zKs=bcx`YbOVbcN4XcVf`FQB{O8
zAB9gBeJ#Nb!A}dr04<Eic%zRProXeIgI|xO?}60R|31hk!I0@tm<J~v*kyL`Z@Sud
z1IcYab#*kF1cql&Y~}#PCaU9kKRkk!b+d-?NZcDm56cwC0I_e0;!ylMeYdo6<B$UM
zdTMVBXyhkD%2th%XcF?ByQ6)YpS?QU8>}EZ3T;}1dpzq<7dK0tyBB){&(2Qt)+eX%
zsq>@YQk2veOJe6I=_D9BUUVjE!YP}h=PD-AG{B6cuTC=i_yorTM@owkt8uj{8g$Hf
zrk|TuAVTTrU!dN#nkLE4?Fv_QeE+_KT<7q@EEw;1eTH|=4hiBDFqjY!%lYS`E?#F8
z8TN@pF{AMre<wc_&hTc`c|2=(0Xd71CAtYwP;wQEB01EirLWZ>?OeKZCIN?ZL+p}O
zWVrh3TqTVl2T`oF*xSEJ=f#Tb>xwwcS7a6Z$aVP7uu4PAdBwQ0U9IS>o1{^(48>@K
hBc4~F81mNKAZy;;Icr@0WHpnKroF=pj>Uf&_kWQ*(MbRR

literal 19907
zcmcIs3zS_|c|Pad$K07K0zoZmaE&ArKtPg+6aooMUL^8J8xmcOP@G9-@?e-rW)cY`
zMQj&FDy<+?q^0Fy7oa>_iXnon0mA!D#DXlLk(b4`fY_o%?f-q>-e>Q7?!6&&EoZIl
z`On_}{{QcP?8n*rOh$$V`i2Kr4h<ykC!IYom}HC2Ts^Qj=}1$nwIVZ`?Rnz~QKQjl
z%-Fc{^wmQv2gZ_W)|X`2%#o3y#OQwZE@${vO)B`sqRf)r%ackg2hosJoK_=CYe&}&
zBqxrn?OVHYWEhQUHho4?GU9_-=5-Yqc5M1u6Nj)34hk0pRdZN-#;|rn+n$8=UXrzd
zrV+<c5fBsH1mfZx1X>ATcw}u1AlCanC>uWsWevqXP@9wn`-a8_Kqd7??RQ?!+WoT(
zLM47=G?wnYJ~39aH+oH^c^@P>5#=5eP)=xP>BfyT<s(^U8VYuvd`SDY9bdjSZlnwP
zhL^PhIVA@9QJ|SZko%GpJV7PMfVTi=(j;n}kY!L*XguWPoiy(F@-+>uL_0V#+BY<0
zfO``HL@xgU@iROQbd3FD0DLsD9|&?L^Czif>k}eJU7fNA)~_5}i-EGsvJXM$<0*SG
z$OX<X)PI2F=Ze%8#Z*eyG%D<4FRSZU_t=y}q2pAl`y|NEkvt4!Uo<M_pS~JZ$tUbz
znl@(XbV{9?Wdm#c5HPC2<eedy2DztG?U5jdNgf4qME147afG!NaqKwn3XfzMP<q!V
z*$E1yv)GT8jn!=4lq5<u2HGm8Qb2~s%$s~P9?}%jX0IGux}tA%`G8qxGoLj?Gt8H)
zKkJzSEP@7#Oufk2LFBAH8~Q%qoWxwPfn;o<D5(>lVvXnS2m@<Nv;sI64h$CZ*#$s(
zN<NQefr*lJC#~xr!_*a}YB6peC?sUfFj-BQR75}-vC;mL*SXNTms9&;x>7IV^t)5c
zl=`e`O>QT7GRQkfo&xfFB>x!X_ep+^nYR@cce0`n<URY-=7r1>u3%-DT=L_w62$=x
zTv`)v^%Ag}(TLETwSA2S&$LJ9ZR)@zgoVt_C=@JlHLp#cRVB3Lik2GfGS+nW4zFD~
zcIN4npNFg;{K<b?tlEr&kh)ZmMFI8ptO{y+n=)tD?WtzVZ4}whS{UKd#i+DP14<q!
z)j}R=P&jX}6P@jGjaX-97aTqBq%%*4?NM&cwDu(3*ZVuo=SAp?=9)m}bHVxs(Thg=
zh6{7MWKXVUv#7)f1vT?Zj9AL_F~WRL9hw~Md20O3CgxYJ{%jLk#kfh+MJsFrH@fok
zEBkEkWj}T802cUJiFIOHH*n&>Ty8NYF#daK^HB#&H)}Q};GA<poFhzt$;>Ow!X!Bs
z{@gmI$4_F{`CRoNYJBS+PJ#PHAy7s@bB0zH@^T&|CEbiCb^V1srl*knOEwkNUPzI#
zcy@*k%gS}5g`J4`oE_-xU>NJVspdjxTt)J0AWtKCk$6!tBnU@S5ET<IAM+{x0&p@)
zbJnz6gwnG@0w|RU2|%>|Q0-qq%vmJA9>_~T{t0Wp0rG4=FOdZzN|Zy6{=8C_qa}xV
zu|3#S0dLJ7S=T>gsbZtil9qN=lbXy9j*<)t{%Z)jpcs$wZMwJ!xnBUmq|3Fo%7vE7
zQ!4*kDE}tOzl+&W{rAFjaT4vcBa#k){%#Z+2A)c9&=|Q?(IiYiuUuwKa@7foVjsC(
zMY@>*ElixoXu~@AFAZdg=&yj(%_Of3<W&-birY|ZA;UM-85OtpWYKnnXiHX~bXRN=
z1H(N%boB*lic_|X=KEk86HS(SBQIw)6JplL@Y>P7)g$gb&l<vRCw<E7YT7{wbg(co
zHlqR8n2hu(lGg_ETfx{LqV`{VP;QIl6rxAVx{WERo4Hd!q%X+C%VlqForadT?rP(7
z>8{D4IqUj;>NA><V+%w>2&3VN_p|g3+H(WQpOd^1<eMaK3K9E-X6W+?Fl&eowV=qC
z@arIgQLw$Xp`X$s;j&J|Knmo+AP1CO{tuu!3FaRIc}v_4)m<puB667^c4lKMM$R~R
zVEyXRfw3{Xn!9+0z+^qvEsm5T<AaiY$eS7PX=Z96yT~HZFvLw}hyqaVt4Lo*l-hvN
zcftA=(qnsr%+Q4re45-0HL?4rwsQZB_U;cJ(rooz2%Nzn+#bj~Vo<2&tHv?GaDu{!
zW{PK@`dxT)VerBK!)@MUTY|@I+E~@fU4w-IMZFCA43N=^bti-k(pz^0@@|mJS-TD7
z3i&BYo8a|44UI9$#=PHhJ!!*y82S-}vfo>_6%v#Sux#D%(zPuI<GIL&V2<V;DAX{#
z57fCte}5n!PzO|e3B@KMy;%?nvmS&c-6-lLJ;Hmfrhu?zzFyJ}p>p&gh`EFa9}eUr
z0U@>;*`=DrG)1I>yQK*(IIpy#72F5WD2Lkn^s0h0=TVmBPd*P505_squ88n42)T~r
z;~=jm`2@%tdaP`iljyB{6x|w69}GBSCE?zuk3xpFMTQaX%<)9KBRCYo(|}R3h~@`C
zqqoPWK;Fe#tZ>=gMU1YSAL$QKst2<jDhQ@`badp5MI+V_&R?xDtjpPUVDfJrlqzt0
zKq75aw4cG_b|U&wAfE;KLxGDrcvwH4KwK#DmFj795xRu~V<SVKA1Fk$AKck1hReNb
zGM0p9K-;aX&$AQp{aYY+$kC|yDT;q5!%sATQSmcBunS|SWQ|ET3XUB)qQQ>mtSw4Q
zoXfP@_>>IuQpf?(V3B0fBJY3AX;$@#JS41ALF_M56v>wY`Enp%$xT)-O((FvRAskU
zL3YN&veaW$@d%LhHUg|ZDZM|Q4$CbjefXt30cF~zwIVk^$Lz0ylcyo27VL@*SgPuz
z9U428g#;;-l=ekIts08xqRAjoenh+gUiTJkhh6K|7Ea_e1cGXair*^VK>wrYzMogo
z_NI7IJsr>8dZT)Q0Nl0*jdOt|)jPs@U@Xn$#KLOg<YUmBHthQ3RPuRKUWY&q?&gyU
zcOc}?4zLkzb3j2;-U6N_B!3C=vm}27@??_#3-VO|vIrQ=sc2g0XC;pwXnINT7w7?v
z3XVtrKa?T-EsjH)4S4s5A4L9Z=+S%dZ$NHf?QcPD1WA{c_)5%~rF0H!u@5NyS!}TK
zl!j0Q4X)5&HYwl~=WTr3gz!9xha_tjHNP{ss2HD{UpU96WqT}LP9P{sS84#@o!j%N
z23}0kxmJ{}2C4O(o0v_0qD@QSVWP}gvuM7(nvHN$As6ns+{#H)h`&zFxOXevNU{d<
zCaGK{L#-yM_gIl`Lm$`A&G)76I0#}OFS#toxfK^sf0&SBBnhGIl$MWT9cVaq^V6c<
zuxvtTbHeFQ1XC?qniEWR>0U3Pl#c}Et_}y8%&FLg6M)`>o?Gbv-20X8Cb>Jo?tu!v
zXqN5)c`w`c3~di!B$u#dac$#3K0>y=Kt8VIT4KiNpi*bRA(u45D%lF-PD-x`sgCuC
zls?b=Fk=;4We0*@`US({(lM=DRi2J?G`1)2;AjoR{HW6oAH(6YCSBq*K`xhLziLDg
z8c8le>F)uD$h|>U=#&qE<ieDG7-R=)$J3+xpn}Ik<xY@YZ2Jhv-Mt%OYCJ~Gt7z|z
zj(@c@X&!3!o2-GD^1%&$`v9u^(JB4*&Tb1%QaJpsMJLv24-|wG>+&&Ce(J8RYz}p&
zymT;5eH%}C=~h`xQmH}Dd=!YMk=z&LbdnS4%N|tBKz5e#)>uA<ZIeRVEVj)KZTo>d
zmTdcjoJaBikjIh4t!DYek8#YOtuuD6(())t*&31PSY9R@KrWXJAXhP@=?9qLOoN1z
zZ3kI87#sFxKRjyCs9Sw!-N=k?t3fGM{qX3vnkvGqnP@IAciog74U*;yUZlR#$=$LN
zp^vDGGVAEAgP{Kck_Uslh~y#It(7sumvMAk{yJ+XgZu`C+cZx5mA<j9Iu4|ZFzUG+
zl&?bngo%tww=w`lKI<N64{qZsWBuCjj@J4qE6(lM19B`az;s`}g(R+k%ikgSNv0bv
zi_4ptZnuHlqOtsTe5+&isrF7ZXeHw&M_5zxpRA>sOuxEc7pdS-azpg3DDa|MzE4}n
zrA8;^``MkYLwC9EzWpc)w?Rqyo>m+b^a!rg$fEdE<M<FEw3nat`Gunx=k7VY+~2j_
zn%QuyC@+6pb3dcWdBG<empAGzp^<E)G~FHnKrh3hbQ(y$1*J!Ue3iA+nT0<?#ebln
zd(#<oCTEM+NFKwOVFOymhPeEuV7)F_m26=G1{Rh4z>=cx04z@U$yAb)z=-`tvJY`<
zDC4;sMV-+~;X8G!*uia|o)qfK<#zRh$a0Sr_7X$!DDYDmXIl>v@1KY|Iz^K*9<@68
zNF7cFw`F3ec5!6ni=~~e=3?F4pqNpwf-%RmR1Toq=Yl+lBtTXUCOIEYtb82BAw5>6
z+a_k2`{qQEbs1PWQtqZsYA|kdAm1pAsPy_5x4@wxN*AUFQX0RuN{<8oyhvUd71QZQ
z6#hyvosEYyU9h?@$v?GnPxeKVD13Y*%03Mefe&v)IZL=PT`)Rpgtx6G%;bh+iOOec
z$eSd3^$*X4tsV0s<EeaxZd**!Z&vZJ1jQ+GVR-flu|%_u-q_@pphAg3>vL}|l{dF5
z26T#N;O4fnObm~bffB_U5S&679>FOw0%;5ggvcw<KsYl-Kn6wK1PZ}fF#@#_CtgGr
zjP{O=jV!f2Op~)ObVn4G3!T?n!iXvZN!SSkK;teXi4P+xB2Ojh!=jF%dt_x)8Ayqj
z19#FFI==1QdXsl+5JOi;S5z6u2nNF)TGZ1^gfqF{Dg};mAcLC3#AsG<M;1y7%~qj<
zWErnEe<dH^A_w$Vd~88K!NdUdr1jQ2vO8Seu0v&xoB+tdz{y}zc^<vlmc*__Z5C9^
z_j(Ssjjp1&*JAfXo{1eE1O!Yjcf6;Z^^ZpQ<)6s#s!*HSD%-L`xTLZHPh?d9A;D}y
zfp9g1AO^vp#r~^)7=6OZW1sW55V%FpO%XwzL{O84;{1lM45GP?GlmL|q|;#PVSf1F
z0gHKcn&K9o4T3#bYiv6m912*;iKKe8H=5H%^%y<|k=P_ukMJU=dH;h;F(V~Q7Ooi6
zw<6KJ659h*-BO3{YpkfA6x*}7pd9mfb%|HLxWOK4lCV5=WY5V`;7=L4wJ&iurv>>~
z6{?H9{3XrCQHhK@zP)idlq48;21KtBVjKe5#!@*DnDgf<H<9v;Hj*cSE9tg>)%83u
zOjo0#x*^B12;V(7`x#t10V2h`ITJnqRDx}XiXDSnVRHo0yFsFW%t!y~SID?Y{F_*H
zeje*K5a<K2;;_Lk*{w)7T2Z~Yg*O6o5eqweZv-}ZL&qij2*lPh+hg>$@C7?*8x#5y
z4!?!E+IvKrBW{4bF*>KM-Uyp}hnKb4p;T{Gmh&!B=}4J;W=?2_at;LFN(5gd8RtG;
zf2z0lSeb4Esb`;?w~2MDqyej&Umj#lG!rX{?`^8i1>+LAdYcz~dn{ODBte2{4Xcw_
za8&JF(`ptA_7jb^2IoTkPh!hoLe0y;ay@&1FE#0vhXX$@JgP5w{+DBe$SQuu*MV)f
z`>DR|c0bj(T|`41BNs=Nfs~etVM%egUwxY-K6i8ES4c*N^BAL}nj7Mtogp1*Y>1Xp
zIy4TF!mMS~`$>>YS;sgOd%<vl^8!(gzg_6qJq~p{DdWM(zc!E*-zS(}T*iY%RrF20
zMeY)3Yjo8eb&b*C(4%9Dw+I$AIe_tuIby#kd0ijKnvO#G=<!3qPWv2-KJ%!@<&7<H
zttUN6HhwpeGWK6Z|4;jX2X}$Z@yS!gCiFYiJFPFakzh2xt1Byt{e9OJ-lgD*y1Gf-
z8D$Gw8>0eFcBWAm0o>Z=nS4fI798+xh$^8p{Q@euFm!CtOwJE8JI)RcZnJ|39`1&S
zZi2xvS;x6;JS;xB34G^Uk$>XWaekZzG_RXw&Yz%v$NA2eNxqK=&W?HoSGI#s<?KO<
z@Gpgi%i8!-aDp$dVm}sIxa7-j$hb<ryf~o(2d2%kC`T5SMY;2DAnW=T?ksZWPU_f9
zKtAC%%c=Tq(7l6bii*DGYn(-ZINXtTY@r3Y{G=O@Ht#G50h<KFdi(B;DeXQd1x9X0
zx}(fD9>pqRg0`gI$YjfYyti;4Y<4{Dx<%<g=zN|WfeNJ7zbj2e$J2~ILfY}P{2ji9
zp3)?lVRhe$MB)PJmI}zgX3zdMszC;7G-<@>SQ}*cJ)X0k#sp~X#70@_jE30mor{HR
zp7~e|7L2y=Zf#tQzj*M&n+tck7Ac}juQAcJaU`!L8BE|NJDJ!dIr45K*&SaJYLFo}
zG|DhFv3H#e)<)=@TX*K&X0efXBeCzoyK~mG^6qiY2fFTMq+JcoWd&V$16-&J9(<Qt
zJ1%%a-t-@AQ<5ARNm51VBkx_{wbMnh_E514-f9pdM>)X|qly+{XrY@UaM&BYLb;(`
zJIBf4VA&(MBpT{bVCkq^Ol9pHlK(_97%fNX>N1%SWXd@~=FSqXu{Z3ChO<`Q2vG~G
z102PmS)d#yI8g8|lFZ+S7S9rEx8ho?b&_QPuilNen9iEsjlLU5ysOl1;|gh)f%q8@
zCnx<Rt<c4gwsEw3FZwnA@Bwd84HsN<)`Wxn4oI;KXmy|WhrEGG|ApZ<uG+&e#@~8n
z(Uo$1&d;}o$~1JclOTq^_RIu6qTt52(EL1`X@M4q??Kyx%%y(@sSgIe5AreAZpE%T
zy%QCWGgWI(fPNA#t^EMSQ{H3XOb()cP`z?qvDR96?N$4+QMDKJ=8MbSr1qM>2$M;u
z>ks0<p+2<EU!L4y_5KShchB|iynY|V;a?~2z<0sx_V=UuV_Ej{uJ0UIaDC^V#O@-~
zxp&d^_duntX6^;4&l2tj$xG<;0lNM{RMhDD&Q8!>aDC@{Q0&&=`YF_B^~s5m>!Vt0
zN$0AGtP$X1tx`n6!HrPTx&O|Bb0Ro!B-VKtB<CYyo6$Zv*aL+>U~WGgq6tyiYp--n
z?#_7xteqDo4|zCmc7K2zF~O?zF>uZ%`8dd9JG0~MZ>!p?`6Epiu7o{pRrWVCabj3t
zo!lW@0pw{-Jq(WhHE$CfJ7Jd9V^QL$Gi;Y@a;CGKSm>P)b>JS^{xT=-0%&(x(Rr>I
zjjTN@2G-J5cZ<PFlcy4%fOWMUoZ(Z9JQD(Tjnm?%2fh{z4MLbB-ahwA<vuNIV~0uT
zyh7=CDa3VN(eNgtUcpFyqL4lV#&6Te63BI}*?xq!o0}A~%f`?pISH`!@dNLYOU+$q
zSYG&Tr=}&FS$f@nT+wP3h!UWXG7r;&kb{L$vE9LdS}`$zm?}H@y+QgM$cLKJzMv-l
zW;(Vkcr_nsFE**<TVmqUUaja?Q1M!1NkiI)9)-MqE7GJnDZuf`-{oHEl+E<M&y*I-
zoIV@INQ+Dgc-lrCdP-7el+W*=P$~E#*&-v<rO5VElhCza%!Uf`Dx}y%E*>5n8Cs@f
zDtxloYE#k2<%yr-LY+d9`|OCwTWC%uhYG&^iQlhoT{FovqX(=TU=(k%s6xYDhB5W<
zJxAA}B=J>8*YA`3FOY|md`*B*aRe(~Ckgwza0k?NBo~|XaJRx*RZ5mm6J&`jLJhJv
zh?_}qZ=kjTF)C)En2ll%iunv)B|F0@!5x*vvq4$$0xv3)Ayn})jp1-3zsD+*A;=m)
zF^FQhU{R1R`vi^x0=QwaMef8}-!&Ut`f3oYUGtR3=Q$9liZt0lh5hdlJyzR<Pe&t<
z${t+;${ziX0QxSD%AiN{bd{Ldq|8A(7Y?OD)lJx4UoB$SCvvnfl40<M2Lz7^6S+_D
zbYWcK21OrYz5yB4Ch=A&*XWZ~x=MQinWp7vHsE$$iQ-$3lj%KVYXl*(n?TuJ(+Yaz
zU#h)|?)n}l9(0AzS9f91xltA7?!qW^f3(CH(n%%Yko$=+%z1_J7;p3u!}OO{bn)x4
z^j9D?^}h}B0W$oWe&xYQ7dDk$522!SPmtR7|Au7I{TyxBM0GvR0s17!?S6O!lnt|n
z@uU>Tp`JvEUPkxF7$Ekgczhnv^&D-tv~lB*wx>S0XyhkD%2th%XcF?Br$#C3XRo@u
zU<rPXItm55$FmM~@xKnKzpv;L__N-HF8bsYHr3w?E=5V7HvJa0<0+m-KkFcB!YP}f
zXAo=b9cH8^Bz0t;*asXbZAPrd)q};1XZpEm1@e@R{srnSt7(z!+^%pl+wQH^EiiN{
zW<gy#H)eSKc$yK?_#H+>eR0v(C3=9cBT<MzhKZnlEJ?gh)IUWMFG+QGc(f`?2EX*x
z2O~MurlqglAgzz=8YK9^KAE%9yTHf{?`ic7(g<<|inA>C_B*M6L6LpcEkUU3hp9@d
z$aFd(XlUz2>znOnMZIB?Mg{Kl>uVxE;&~m4(>$6>gyyYXL*w#CZ?Nf{;bn92AGiG<
DM|i^C

diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp
index 24cf908b2..92c0702f8 100644
--- a/src/frontends/lean/frontend.cpp
+++ b/src/frontends/lean/frontend.cpp
@@ -559,9 +559,7 @@ static lean_extension & to_ext(environment const & env) {
 */
 void init_frontend(environment const & env, io_state & ios, bool kernel_only) {
     ios.set_formatter(mk_pp_formatter(env));
-    if (kernel_only)
-        import_kernel(env);
-    else
+    if (!kernel_only)
         import_all(env);
     init_builtin_notation(env, ios, kernel_only);
 }
diff --git a/src/frontends/lean/notation.cpp b/src/frontends/lean/notation.cpp
index ea0ce9ed2..563dbb15b 100644
--- a/src/frontends/lean/notation.cpp
+++ b/src/frontends/lean/notation.cpp
@@ -17,7 +17,7 @@ void init_builtin_notation(environment const & env, io_state & ios, bool kernel_
     env->import_builtin(
         "lean_notation",
         [&]() {
-            mark_implicit_arguments(env, mk_if_fn(), 1);
+            // mark_implicit_arguments(env, mk_if_fn(), 1);
 
 
             if (kernel_only)
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index bd102d359..bafd1089a 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -106,6 +106,7 @@ static name g_push_kwd("Push");
 static name g_pop_kwd("Pop");
 static name g_scope_kwd("Scope");
 static name g_end_scope_kwd("EndScope");
+static name g_builtin_kwd("Builtin");
 static name g_apply("apply");
 static name g_done("done");
 static name g_back("back");
@@ -116,7 +117,7 @@ static list<name> g_tactic_cmds = { g_apply, g_done, g_back, g_abort, g_assumpti
 static list<name> g_command_keywords = {g_definition_kwd, g_variable_kwd, g_variables_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd,
                                         g_show_kwd, g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd, g_echo_kwd,
                                         g_set_option_kwd, g_set_opaque_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_coercion_kwd,
-                                        g_exit_kwd, g_push_kwd, g_pop_kwd, g_scope_kwd, g_end_scope_kwd, g_alias_kwd};
+                                        g_exit_kwd, g_push_kwd, g_pop_kwd, g_scope_kwd, g_end_scope_kwd, g_alias_kwd, g_builtin_kwd};
 // ==========================================
 
 // ==========================================
@@ -2554,6 +2555,7 @@ class parser::imp {
     void parse_universe() {
         next();
         name id   = check_identifier_next("invalid universe declaration, identifier expected");
+        check_colon_next("invalid universe declaration, ':' expected");
         level lvl = parse_level();
         m_env->add_uvar(id, lvl);
     }
@@ -2566,6 +2568,44 @@ class parser::imp {
         add_alias(m_env, id, e);
     }
 
+    void parse_builtin() {
+        next();
+        auto id_pos = pos();
+        name id = check_identifier_next("invalid builtin declaration, identifier expected");
+        auto d  = get_builtin(id);
+        if (!d)
+            throw parser_error(sstream() << "unknown builtin '" << id << "'", id_pos);
+        expr b = d->first;
+        if (d->second) {
+            m_env->add_builtin_set(b);
+            return;
+        }
+        bindings_buffer bindings;
+        expr type;
+        if (curr_is_colon()) {
+            next();
+            auto p = m_elaborator(parse_expr());
+            check_no_metavar(p, "invalid builtin declaration, type still contains metavariables after elaboration");
+            type = p.first;
+        } else {
+            mk_scope scope(*this);
+            parse_var_decl_bindings(bindings);
+            check_colon_next("invalid builtin declaration, ':' expected");
+            expr type_body = parse_expr();
+            auto p = m_elaborator(mk_abstraction(false, bindings, type_body));
+            check_no_metavar(p, "invalid declaration, type still contains metavariables after elaboration");
+            type = p.first;
+        }
+        if (to_value(b).get_type() != type) {
+            diagnostic(m_io_state) << "Error, builtin expected type: " << to_value(b).get_type() << ", given: " << type << "\n";
+            throw parser_error(sstream() << "given type does not match builtin type", id_pos);
+        }
+        m_env->add_builtin(d->first);
+        if (m_verbose)
+            regular(m_io_state) << "  Added: " << id << endl;
+        register_implicit_arguments(id, bindings);
+    }
+
     /** \brief Parse a Lean command. */
     bool parse_command() {
         m_elaborator.clear();
@@ -2622,6 +2662,8 @@ class parser::imp {
             parse_universe();
         } else if (cmd_id == g_alias_kwd) {
             parse_alias();
+        } else if (cmd_id == g_builtin_kwd) {
+            parse_builtin();
         } else if (m_cmd_macros && m_cmd_macros->find(cmd_id) != m_cmd_macros->end()) {
             parse_cmd_macro(cmd_id, m_last_cmd_pos);
         } else {
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index 3085662f9..f76826dd7 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -59,6 +59,8 @@ public:
 };
 expr const True  = mk_value(*(new bool_value_value(true)));
 expr const False = mk_value(*(new bool_value_value(false)));
+register_available_builtin_fn g_true_value("true", []() { return  True; });
+register_available_builtin_fn g_false_value("false", []() { return False; });
 expr read_true(deserializer & ) { return True; }
 expr read_false(deserializer & ) { return False; }
 static value::register_deserializer_fn true_ds("true", read_true);
@@ -114,6 +116,7 @@ public:
     virtual void write(serializer & s) const { s << "if"; }
 };
 MK_BUILTIN(if_fn, if_fn_value);
+register_available_builtin_fn g_if_value("if", []() { return mk_if_fn(); });
 expr read_if(deserializer & ) { return mk_if_fn(); }
 static value::register_deserializer_fn if_ds("if", read_if);
 MK_IS_BUILTIN(is_if_fn, mk_if_fn());
@@ -139,17 +142,4 @@ MK_CONSTANT(abst_fn,        name("Abst"));
 
 MK_CONSTANT(htrans_fn,      name("HTrans"));
 MK_CONSTANT(hsymm_fn,       name("HSymm"));
-
-void import_kernel(environment const & env) {
-    env->import_builtin
-        ("kernel",
-         [&]() {
-            env->add_var(Bool_name, Type());
-            env->add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
-            env->add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION);
-            env->add_builtin(mk_bool_value(true));
-            env->add_builtin(mk_bool_value(false));
-            env->add_builtin(mk_if_fn());
-        });
-}
 }
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index 5f820880d..3bbe713af 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -164,10 +164,6 @@ inline expr HTrans(expr const & A, expr const & B, expr const & C, expr const &
     return mk_app({mk_htrans_fn(), A, B, C, a, b, c, H1, H2});
 }
 
-class environment;
-/** \brief Initialize the environment with basic builtin declarations and axioms */
-void import_kernel(environment const & env);
-
 /**
    \brief Helper macro for defining constants such as bool_type, int_type, int_add, etc.
 */
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index e7d51f9c8..49b668ec1 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include <tuple>
 #include <fstream>
 #include <string>
+#include <utility>
 #include "util/thread.h"
 #include "util/safe_arith.h"
 #include "util/realpath.h"
@@ -380,7 +381,9 @@ void environment_cell::add_builtin(expr const & v) {
     check_name(u);
     register_named_object(mk_builtin(v));
     if (u != n) {
-        add_definition(u, to_value(v).get_type(), mk_constant(n), false);
+        auxiliary_section([&]() {
+                add_definition(u, to_value(v).get_type(), mk_constant(n), false);
+            });
     }
 }
 
@@ -701,4 +704,26 @@ read_write_shared_environment::read_write_shared_environment(environment const &
     m_lock(m_env.m_ptr->m_mutex) {
 }
 read_write_shared_environment::~read_write_shared_environment() {}
+
+static std::unique_ptr<name_map<std::pair<mk_builtin_fn, bool>>> g_available_builtins;
+name_map<std::pair<mk_builtin_fn, bool>> & get_available_builtins() {
+    if (!g_available_builtins)
+        g_available_builtins.reset(new name_map<std::pair<mk_builtin_fn, bool>>());
+    return *g_available_builtins;
+}
+
+void register_available_builtin(name const & n, mk_builtin_fn mk, bool is_builtin_set) {
+    auto & bs = get_available_builtins();
+    if (bs.find(n) != bs.end())
+        throw exception("invalid builtin object, system already has a builtin object with the given name");
+    bs[n] = mk_pair(mk, is_builtin_set);
+}
+
+optional<std::pair<expr, bool>> get_builtin(name const & n) {
+    auto it = get_available_builtins().find(n);
+    if (it != get_available_builtins().end())
+        return optional<std::pair<expr, bool>>(it->second.first(), it->second.second);
+    else
+        return optional<std::pair<expr, bool>>();
+}
 }
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index aa6af8251..a9b0972fd 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include <vector>
 #include <set>
 #include <string>
+#include <utility>
 #include "util/lua.h"
 #include "util/shared_mutex.h"
 #include "util/name_map.h"
@@ -411,4 +412,21 @@ bool is_end_import(object const & obj);
     Return none if \c obj is not an import object.
 */
 optional<std::string> get_imported_module(object const & obj);
+
+typedef std::function<expr()> mk_builtin_fn;
+/**
+   \brief Register a builtin or builtin-set that is available to be added to
+   a Lean environment.
+*/
+void register_available_builtin(name const & n, mk_builtin_fn mk, bool is_builtin_set);
+struct register_available_builtin_fn {
+    register_available_builtin_fn(name const & n, mk_builtin_fn mk, bool is_builtin_set = false) {
+        register_available_builtin(n, mk, is_builtin_set);
+    }
+};
+/**
+   \brief Return a builtin/builtin-set associated with the name \c n.
+   Return none if there is no builtin associated the given name.
+*/
+optional<std::pair<expr, bool>> get_builtin(name const & n);
 }
diff --git a/src/library/all/all.cpp b/src/library/all/all.cpp
index 703bc6ad3..4536ddc36 100644
--- a/src/library/all/all.cpp
+++ b/src/library/all/all.cpp
@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 void import_all(environment const & env) {
-    import_kernel(env);
     import_basic_thms(env);
     import_arith(env);
 }