From a2d2e36f042d461247ee3ed101299424c05870b1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 10 Feb 2014 09:03:42 -0800
Subject: [PATCH] refactor(frontends/lean): remove notation for creating tuples

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/kernel.lean            |   2 --
 src/builtin/obj/kernel.olean       | Bin 51377 -> 51235 bytes
 src/builtin/obj/subtype.olean      | Bin 2980 -> 3016 bytes
 src/builtin/obj/sum.olean          | Bin 9228 -> 8857 bytes
 src/builtin/subtype.lean           |   6 ++--
 src/frontends/lean/parser_expr.cpp |  47 ++++-------------------------
 src/frontends/lean/parser_imp.h    |   2 +-
 src/frontends/lean/pp.cpp          |  39 +++++++++---------------
 src/frontends/lean/scanner.cpp     |   8 ++---
 src/frontends/lean/scanner.h       |   2 +-
 src/kernel/kernel_decls.cpp        |   1 -
 src/kernel/kernel_decls.h          |   4 ---
 tests/lean/sig2.lean               |  18 +++++------
 tests/lean/sig2.lean.expected.out  |  18 +++++------
 tests/lean/sig3.lean               |   6 ++--
 tests/lean/sig3.lean.expected.out  |   6 ++--
 tests/lean/sig4.lean               |  14 ++++-----
 tests/lean/sig4.lean.expected.out  |   6 ++--
 tests/lean/sig5.lean               |   8 ++---
 tests/lean/sig5.lean.expected.out  |   8 ++---
 tests/lean/sig6.lean               |   8 ++---
 21 files changed, 76 insertions(+), 127 deletions(-)

diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 953247847..48a19db34 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -778,8 +778,6 @@ theorem proj2_congr {A B : (Type U)} {a b : A # B} (H : a = b) : proj2 a = proj2
 theorem hproj2_congr {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x} (H : a = b) : proj2 a == proj2 b
 := subst (hrefl (proj2 a)) H
 
-definition pair {A : (Type U)} {B : A → (Type U)} (a : A) (b : B a) := tuple (sig x : A, B x) : a, b
-
 -- Up to this point, we proved all theorems using just reflexivity, substitution and case (proof by cases)
 
 -- Function extensionality
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 67451cdabfc4521935c3982885a894846f6415f1..1f25e1e0c44f5ea921bd8266cc88230dbf6396ab 100644
GIT binary patch
delta 7464
zcmZu$3wTu3wLW|1oXpHQC&HLOCJ-h-NJ6M$03~4LWkQ6?vw9JUNP@ta3Q-ZLS9=@0
zpV&_&Kv<v`3qnL5@(zkXQ7exiwLZ|)dutJlrBdz1THE{8+otWk>tFlKoJo}L%bI_$
zwf5R;ueJ6%`y5)Df?L-F4-`Fa*FI<j7A&ow|KJiDvbqPIe0-|<Ib}UDzTiEB|EUm@
z;QK(9z&5~);vm>Rr-z>yuFlfIC(3d@0AJNEtgC&%2)uL1C=iVg);>8gw~|E$<{1f)
z*u+Km;Wv1W<~}*DOr(hc%m|+aTXe9L5t9Xf1E}4&2sm4~zolP4S)is+%kmuc3H4lA
zp(<(C%ApfJ_qBh|&>Ae-{|#=)2~5MU5xK(&OsF*!@a<UGh=U|RLV9QC=$9+|tIz1`
zmA4H4Bly~ZuYhzM{=_hHPs(i-3I!g7q7f^Eq>`35_Eld}b7Mu$*I;V{|LeoQQb%K4
z$0i0Y9JR(KWAhgpx@t7<>HbxPbg?lS(!2gA?OT<r9;Gv@`nY#tQkyLH2z|AxFc9pZ
z*y_#G1K`VQCQ_i?HBE+*CahtCMAj7nB19^T@zY876WV>|8B09l;WhC=n|!$>wgU>r
z68?*90;=&GHx*4=bB)_1VVwl=I(l-=&>OlzNqf~DNP=iaq0j_ZtYv`fK=y<J6ZjWC
zVkx$mKPfK|*+V%^<JBgb-4s)YXj#*6bp`Eh8eP^0y4td&F)W+R2R9_JFQAtdzy$wA
zrcnR26)KMwti38T&scJ|5vW@*XUXEF^Xa&oNBfi=iovbO`}Ee@c+Nn~(`%Ff2F36o
zQj{IiDX648x+&^ms3512U(phpI{lnqW5R92IFN<t8VH8gMV&{^VWq&eU`kqk+ePV|
zC{fkZ1r3qkh*{r&%vIHxD+Pt~8_`w^z|@*pKr6}l7Kc88=C5HcQpv>gy%^)`Wh~ph
zDk&1z$|8DJny8EK?c!e<tbB;663-9mi*@nnd2uKuihN9Y>vKn(PpOtk_fS$~kq^7r
z{TPuk2g4+i5xGE%*5^60Zy8t9y7m31T)-06NhnkUn*9OcNaWmrApfWzG4b|#t`MBy
zXFlgwfT3hj7nAwasNv{>I<!&**tvmuUO7nCbdg-=bBA-0WaZedf2<_ruphaDnxD#U
z_=YGHSd95bOb0L=sFk5??jvuc?qy!&0uwtbYEt_!ZMztEEib#LsCEvejZ<-DvNA+L
z2-nwuhMr<JRbF-!bGww6XO#t!&wO#Ju<Ra?+yU}=S~X#e&f|%tf=~-aEX}>|LLpm6
z05Yi_Bso$&2=p?TVIfGb0R#4xDJc4O7BeH&)Ng%OgU$QYR*W)e>C)&@TXq&Knj@2{
z65vQR+=~2}iH^FITFRe5dC0<~AxxwiMDjmaBl0CkHH!HLLtWwlkC^C`+42CAltob;
zb_Ntu)nNpa)i;dPhH~{jMfYcyLq&I=8vu2=jRMqtZ!};?;&?zH2+oQ<l2&ervz6T&
za+$Vnn8@_2RavP%SMp3jY!u=hl&HcFBPi#>ET(zS42+JFjmaTMKv+WWZYZGFpRxMf
z$RoQ#=1Sj9pF5294#)|Z<utZ`_5icEcHX=>i*<P;Smv;<jB*<Glfy+bQ)}5XS<R|p
zVswC<Pm@shjoEcr+>1j6ppHYO561(_UBavaOi01q1lT5U0^oUp6Bz|s1xf+V5QyiP
zJ&PJQ_ENKH=f<K21i}732)t9bF)=!P#~_gcG|<wFw$2i(223rHM4@qLYxg82_QG$G
z=ylEyG-&dsa8#DRC(Sf1*c89+8(g+13wlmsse0HpJ^~5zpFNX~Zt7bpd%6!}*zo4~
z<{^>#_9SvL(R9*0Pf&DAHVwG7M}vJ|=b3&M#SeRNm+ALP@xU7~&xHreRY~){^TuN^
zEWKMVypV^+`OfMFwLV+wrn^9Db9RQ_A@$yz+aO_Dm@*}C&?|#yKg?H<IrVqJw0(Ei
zOh6-&ssMQgdD(>eqOR&Ng3GVn=u5t%(*%(eb(=5xMgr-==6H{kzKy<buL4=d(az2I
zSHOp;bW4wn$$;Odo44fl6#YgX>l>o&iH<*;OJf(C^z@dT()92^QJ!h~i1El?(IrET
zbYV-by*k;G#*u0s!yRN?bG&#urt4$(Js;lU!&@2JyXmp!K|G_Sc`(!V=2+f=&hfWf
zFhlO2b`@>j8mAsRdiM*b!mYbKhThABmQek31^JkoVWx`6*1a$3>@+&?-1XgdCm*EC
zVIoHJoAWb0w`Vbf9W2~BNFAVQTYFuH^y>8_EC~$J)$Fc5pAm_a-(>a~A^CV~EP5yv
zJ$=N^Q26;0`&iPU8C3p!U2j=L`heI+t1*J!rhfK(?ua|V&>en`4{HE*v~e#`{iH?B
z1y^^ryQurNTy>rXZ7XDNrfthjTL{+8UC^!b7J77BLGh<au6-$0h*Hw_rv=bWc)IUw
zo5~jB+w+-@-d@lX^Q`~F6x~fwJ@#kR_tjpR9Wv4DeDv)0fuYa!8Kt+k$K6Y;XzubD
zUvD3yJ(S`T4{=RXle|@@?<i20Xz7mp8J}tn3-y6RZoJ(vvVYgrc_`NLpJR2EblTSM
zcMR=|C$;@Ykas)p$H`!(5uzV%@5j5obLYTNNc^5mjXUG61!0}XIJ|Sr2+65zM4Zzb
zVIBLQenlYV4rbbClLaxG2ES0p_W6Mv4f(qavyzdZ_g=`RvoG`>DP^Jy;%-QE6<~+n
zs}7F6_o$OcNn&7-8Rl#nuxqGVK)3Ch>*5-ms<PHyBS$O(LmRCJ)JD-}JfqV2_4D(7
za1#iSb2Sa$Jw`30WlZzv<=ta)mO!WtE%o6ta`#MC56~TZ;%Xv2yr)_{ME|v?bj)(7
zII}{51p=xiJZ1X6@qm_z0-$#dc_@udReKxwMfmjIQ9}^P@ZXt4vVo9ELtl}k0cwxX
zF};`0)iicrul%%Gk>s1ZR0WQC_|LRtU*CGs!M!iyM3|aQO!Vucq{tDUv8aQ<L>z~y
zDpQ60BX3*bzlnuEL1;4x{|%CuPRgUe{$~;AhkU=wQ!8ok{s$XaAdAU!&zcP@y5dm*
z&W~k`XNvSB=f~0k)?utSyB<itVLt_~eh+>cQ0MVK7@5D2X&b<;6Zi}x=P`ys!~6+N
zd#xu;J76}XEuIR3x(%W7p2`_2&7W^oksimNUnb1If2g6{3_~W!DQQbhuxen_su9DU
z3Qy!%B+_)CBCkWCPQgxT*fU{8t{X-W%V;O%$ZbnomL<+MDdZm|^<`;iJ0v@p$OjoC
zcm-hUDo%85%lf;-P67fHi*s0_w;5v{|1CajW*Es3h3CN4@!#sh=NUSOL}44?%i1Y=
zw<VXR9vq^crAH1<=MNrj2TOD+{B_@vSvz4%uloX!&O3U1_z$A68wz^eJ%GrtVeVz(
zt-BBK?Nl(ldp0wrI-PfcFvs!Zu!GjTSkBMNw_Y60G=EYL>bpNvy+ngw`ge7dT3(uZ
z{YlJ{Y33;(whB`mIPJqX0Ns)xQ}d{SCP<SHm8%o<_@PC&{{lj7=q(?<?ZbBf_5Q?F
z4bS@A_ZX`EvMAcK+F!!d>7c1ESEx6MnD(aH!#VVamviEmlkeC2U8vp+GAY@mKcIrc
z!<^pXz>USsH(X4cZeLD{KcQC+mu9DlJzLJ@wMTlZ63RQ0r@o+(N3QAfZ91N^dmXJf
zQmDSB-A5|aW%}~S`1!+mt<X;RZ^<j81j7oz1q~56BO(f>4^gGgW#MKpbiZ4~G=O#`
zcM?~d)y?P&gIa!?O9zh@aMb_vXn$qUUyt5fA;mAXWp(3ey0)zD4BZ+rd?mQjUaTyJ
zq3wKemaB+6caWs>6WaaLhujZXrVk~*Yz#Sem6}O+9_t-`(<l%=J#uV<%A_}s&2%0M
z2PO=KwsSLG{YtL}IXV{JGjxqx`9ACms2A@CD2cb^0jD9X>r0U}fRXez!zu*48RhPO
zXmeK}-F`QAGaxrUqSLQj8~r;b>u<zi2JQ-SUcFWo)7V#gbz2QlvOQRRsP5JJ2CgB!
z2elvSa^9?BDC%^HX$?_{9(RxrzXO<%0AJ<9t9>}whu1LlvRukg?RRL#YdxbY7`v-=
zp)=&L|J!R-CBzWl!F3}>AoN#3*%mx>S9oXR@@q3@iOZe)EM|x@dWO3OJ4p-TJ_(}q
zbu?Ue4HMa?_nFK)C{__|{Mp3Ot7U^DprcD{qz|tL)Tu4^p?vaiJr8x4h|!eS3se~`
zetk^FMQFzGnWREYkHuJ<9tS92zO5Sp<&LG#0$R9x4$Pqb-ux0U+i6+eGhmIOqT_dt
z70dF#O+Y5I9bw9&E%hkY7ppW$0$Ftz)2ZV_8!9nXyEER0RX)54a_Ljn1RqX>LYw4l
z2tPb|;QkKe5{|Rm&crWU3ATGFnP3+x+M5o8mY#^Ic3O3!e-xg3&qdF_<0s0xxBFa1
z?q4W;GEa8yJ?ELJKV^tTtA>aE!&Sc{_!6VTvpnzQ4GpLW_aB<UP#!QcUyv&WgTQvx
z5%Z!bI<8!wBm+pA_kT6!31Hu*`wt97D+m;vNcpEis)CA7m8u$=d8$HPq>ZPF8zc%d
zSVK(`JtpR^5L0Uk#yV3|f#i{DO=IY_z3Czs-S08<&gw0UGOrNst$^K}zyn^&GNa5e
zci}X<i<q#xbYp9lj@K+6XLhHW*0|Ho(DKHQw-yz`NB0Lz<VhsyHStbieu&gc_T3-Q
zFI$UxTny`5tPWQ_4ypAo)a`U!_USHzjhRg3%3`)-y41fgGtmk%i&7a9rawo-X1nMx
z;lKj|`HGpaC^}sZyP8aUPmfc#)0d~KM#?L#ykS^#FkizOKz-V41#$t`&Xxb5b1uWK
zbAsyMsN}r8_(tiKvaqgs`55S2q;c6<ZUQsqP1S7&gNo0@ua?@7Gm5nE$AutM>vmv$
bq1J4#Ru`Ws?KYbw0j0**&#S6iIN$hx=@u@7

delta 7600
zcmaJ`3wTuZmB0U)dowe4E+8i4MM#8@@F+rrK!P9vQy?fpu~zDn1Or*t2UwH^{kpMA
z`94r0aFi03r$9g+3N?UOD}oQKS|82UR)rN=1iGw1bz7~0cF*seJ9CH8-F)Ai`Q7vS
zpZ_`M|G1M4OTxRBhIf`OjMh(^ZiQym&7jT;a&NWxFA@z+#kW<<pXj*=)9{;2EF<tO
zAV=Wa;6?=g7O>V421uAc(R1VOo+S^zVH%>I3ul>k=*fkni$4HY-TeVb-Te_TqZdrW
z@6d&XL(K1~d{ITtN8p>fyJpnQwnFdhwu(jLBYJqzxV-CFX0?GdfaE4dJW9tGjWX9!
z>7zwCCn3?%P66H~5&wy9eYDt2rd<!^m=m<((Q4K{{OG{aGlBM5hE9LcJ_l|j9{K^k
zt=Kdwf2_MXN;f{%!+cKj9{b_szksiU{1r&2^c9rv>&Z0wp2#Dix%|z6mN1D)^b7D@
z8wt(Bw<S-diD~=~?V6B96^jStoQF{TUkKpe>8FbeH3_-kB35T)!n&PW7mwg+eYv<K
z*EUHjI|L|Mu)|c=lxG&xHBH^TyTERfz!uTc=1f}9bZN-8Xl2vdNpP&g+fg8yo*iQt
zTM3!%0j@3u{4XX3TCsJB={5w@z0V(D(c^`ETLL+1YV(Kx?&D9a1*q1aiJd{edwhVm
z5{b0N^Cz~NIxHDDJPXf~6uS$MMwJbPl?cU|1GpMwcO+E9--uC$%Alh01)<n(YF;wh
zw9qF@a?MNh^^zeblLjmuQPBgs>bV#&DwCA)rQvPNBDIPQ{1}@|8<$p_?sRHtKc-!l
zRho}!!m`4g%b~2^`U8f=+W>lhSytq*riRum8{65(P(e9kpVD8KO`LRGhAm8T592wM
zDG^+f<erAX@!k-XgDD00JWc7iDA60si~Ge+i`&3~*qU2lE4}nSbk!?;Mn!j`tg-)u
zk@l@d*bC3qOsrg))D;3jBmgx^k)#FqCkdj0)nmtCgsR1k(aa|bJD-rmCq=PSwC0Jt
z$`eV|3fTutJIrFo()^yn==LDU`aph?&OT8PuTMVLQ}&ZRCY;0&&MQ!;2eeUk2_$yB
zXPB}1S0;Wjj+cNF{ygA(3K&WBXg^x;<W)mH22b*bab-cuX6V;^D45y_R|0A$4C7A7
z9PW0}Rsdg<%OExlkKtf?kbGN{YL*w&e-;hZLEFq^5<3aSe93RJcib*`PVXJJNK}I{
zkUY2h#l7R^ixT%v&&DG0nrt06AEs%o<2z+R?9YK1O(m0a5tB?V_C-n$f%zp9Uo4F?
zoS&`Sl;|3v&`n}MduY?tGl<pq1(m%RbFiYQss$ytYZ8jSTfod%eGr-GL&xpPM0BhQ
zJZpcXHkgcG00VnOLRZqQ{$kjxwFU?(2ro1&;_$OQgh@Clxqv}pUxU<ZOQXm6fr-}7
zb-|Fr=c6e3Zl?qzCOsHV^k5}DvSJu-I{Q}?UNH(f+G<w=>K0ZF7{RndI|YJZQ*y7S
zj?IN^dwFvn)3MFtm@XB(t-08Yp?90JO+Px(+`ID_S*6nH4KVLRlbVZrpx@nVLB^vr
zVKkMlgs`j}yOMVF%n8{eX=IPAo_4>w`uZt9`3aOH8FpnlV<hcfxwo+{Ihc#)c4}cD
zi~h*P5;GYRy$eX+jK#AipaxJAFfM@C0P41dxUB{;!}(&h3FPycr*cH_1m=cb6F8Bf
zJ4N6mz&ohZs(dq@`mQRy3|Vn!gCJUssXYjEHqBa<Ri9MS*&Ja_t4(Txty|4;3R;l3
z_kV{(9Un=Tqz-gyRpDR><h~Rx`;#&Kz~KI0;KVu%66KFuN5fWMrt`p+M56I+0!Q=c
z!PR*g>Yi4v9?&>1MJ8UD1S7c*q9rV>d7a%{X%UPkN>&(s?Mh<dGziaH0LQWqtL6Rt
zXdSs&-8w>MT^8NCrfX?h9J-Fv+hrcDUgJl9Kh?73duyD=`Ful|a?c%b@80|WBo+#?
zw`<v;J||rrI&F|F|1ODylU{ExwM<mIws4|m7hdLq`~svA{(@p@@?_;b4Dln$m6w{<
z8zGuazg?S`Ek2jShg|erUvz$Ld0BeqWR99S*f*tBa5*O~&s~w&dB)Hq>#9o7*wRJ1
z@UcW>aho2pS}>Xwr3arX3c0NmUEeoD4dk|Y?fUG&fjz43-{~2+`;uLtP5Od}wF{{G
zhC=#9OILb#eMZ+b4=94w0OQ!lbZ&id5ezfzWcRuIppZPne?$YHx^h^ne~wxYL8u$V
zt$@0N+!nyw12}~tPipg1eG9~AX|nQuLi`{;e=4^ieKvY3%4}}r*;Mh)Tel&%^GnH;
z>!jbOMH~9KuO?D{3;lY-44tsFVgrKFl>1|i+L(8}G_>x5^-xea4N#{u9n9`hAMv2O
z;6Fh@dsNN|5k15__XKU<SfazWixLP9CoAF)``;UJf@Ewe?uC~rdn*(7Y>*Dw)Xw14
zOIGFwn<lcwx=lq)U*1%l4Lj!_L9b&V_s{gVO{J`GSxfK87k=p{wiJ42S!i$d8S`4I
zQes0u_J>T&ct5tbmSS_3zG^9oobfr`Hs@BHOOK9CtQq`?cTAUD6!%@52VRDg+x;8J
zA1@9#E~j*a{=TU@M}2g2@5m*7i92m6^g6PIHN$5N-BML4ohuo|%JZXU6psXLfYild
z>3*2#f~mA~%MA9<FKm%S0m`2qI#k}~wAgpEfnV%<0QC)KCZIO=EWn1|VW##}YI%B~
zxsyJ8daCz5@WXzd#%>*2DaW-s#ZKZom7_|X%I>UA=RlzWDTxoE=eJgwd+BSY-Klb0
zRn9yJ)zJe1e2|*9O*C`qKeiQ`>*>O_TTCO}w7snA=TM2?5eZEfP%jCo&|3xeMwTTA
zpCmF3+|d$jdSiQ|Sx7ZIu4<H*zwmD$47R8!E^M(Z@bo^u3{ayZAbqcVf?@PbJXAC7
z-YYDF%2|2^&M-((T<6ZnKFB0+8a<yZAYIsT>Ggp!7M1-0l)q#WiwhCuENL^WDqjSd
zsR%}meiOK9BeO6wH&^SokQMdtk?k`+pMLsGfmuo`pPAdJKR(Fe>fDyJPdRLLANekc
zY@}M)6&OIX(+s59SqZK-!M_2j?kYz1Te7*VwosE9g4ZyLHwj$J&^-ICteVLg21-lx
zYbj&={=&H*Xc;d<&UMMSQ_GT+DYSjJ3^NN^4K#9RPUAYpZXGf#mo)8gaTZ)L)uUW7
z(<FNNl&vwoAmKxzh;QP@cng!%_rAnJ#rd6K_>T_mT-;a+Rq2>^q``tzJ<Ar*fJaT?
zMnFwB{QD52#4;p<o55AxEdhL*VZ2ooumQ(+%Sv1T1s)-6#rM*oU4zXAy0B}KX{Cw3
z?31A}(ShAvP$_!{bamiofV9rfGK`)Pzj83>z`LNkK)AnT<PZED;M*4stan<u9L3*(
z5p1mF3(R(Ya5zQL=LVbIG~&4tOpC^Mp~s%-VD{0v=N{%?X^LAXUik*B#MaiuEJMF3
zOo49&@NGb^k8BGsS#sCd-#W}3qW0FiZ+Z_xbtI>-!rukll*a#eaCN@F4<OdBc~%Df
zgTOva<KJ)^tIfOQ?5Q^SG;U9SbDHMvDKH<=lY0im^P{1wd%=a5Pi=c9xu+9Na)SEr
zEh|eA`&W_pX@IEz>tP!MF_%1gy{Tz$f%$^A?H$nV|1!l`<@D9w5_6uqJzvey)IC4?
zp9eELvIVg_8B8=0QfD7V!HkJQEPyV<_-Wx{U-HJGb3(F#!oX9vx*vVP3@*B)y?9?w
zbAW30^)L?Ixo>85CPdO<4ve+KoGuJKdA)LSL@oniFO2XHhBZ?eSYBOUspkpm_QC_%
zAAu!nH+bvfpLV-vW_8lt)K470+r0Ne*XX;Ju6_FQg&K1y4gb}T<4w^}%|LjG-#}}B
zmER~iaG>VLCw??k+4*Isb1-l12&Y#7(eU~*=}0fgM(6ZpX8Z=of*<I-`5tto#~K)T
zj@TZi$`{K!x67D#XOiom$2<9p<&jdcI6~`ZWnSVnL6}%PP7nI{#d{jLQ*<f@OV#_i
zWUn6-rMI2S1K2-+0|HnE*dS(C1W>Z0+(7}ioT1+dC^~QCy}ormN=wXVsn?`SgCSSq
z?61f4S;jEf)`KHeOpsh}zQ3Aof9b}XCEJnolTed`&B}W`ExS7;SF)jE|MwneB1w>!
zk|1&4qmKK>jnFb(1syH)hyYdrYRyLmP<~?Z{0Q-j`To{idU=1b8BWLdSKW3Dn&{i$
zs^JeT$sG-ejx+|)7VcO;xyb2)g1sjV9@by3_d&tR<$qjchn(-zikENCmVuH@q}K6c
z<Q>TCEFwMD(SY8)G~~d*#&K|=LthiXYXdkQa@o|J>jF3d3T=tA8p-uefP5yU`b4B4
z4Ir3}_gV7DhDuzbX}9R)fn4(meR?3PNaTa~NKeZBlh==S(7}pJ;MnKF=U?c7g9S3@
z)MH=mY5PH)vs25eR=e-zgM-6oegoU{$`Bb7Ukeh5CGd0|8AKFC$HP@$XDFqO$Um&?
zL*U8*uBzwhXRqX#8ft!}%uJy-U#T|7sN<`>8j%5m_h5q*OFP(Gkt*khc-ETS0Hj;c
zj~M!!p;&1TPKK^7#ve24&_O)h1lTbin$6c!6sH5Or}ox<O!c2TocY#QGs_W!b2Ah=
zG0_Fl03<{kwv-<|B;Hq~_E$?wVCc<ZVx(0tsJy4xA12kkIW*?A(k{pR9aocaH`cRr
zGyUwfLP>ykKYSo^SsC_Gm`l40vjaB14kgJ_2{W(}v3*o@m{^fsOuT<E2^2eEFA<%z
zrOxjaMX!%Cw^QBgV}{<rO8O4t)CX`HpyqkHK<?4Hsg_(vPb1R!0Xq8n_qm`YhsrLM
zfprJh+u|`Am6b^k9Ex*?12rEiy!-(C$SOq6tOj{Uapc#7RJPx(#}Actn#yV+V@BUo
LKW4^V)2#mm;>J!;

diff --git a/src/builtin/obj/subtype.olean b/src/builtin/obj/subtype.olean
index d4dbec6cdd176d491b044ddc4e6267236f6f7dbb..bc85d570b2856dda4cc1ef4443bec9c59f262741 100644
GIT binary patch
literal 3016
zcma)8O>-MX5S^K|S4u2Fa)>N*$&kb!qymYla)1L6pa`<5f?NXJRO|ApEYMe0Yfw(`
zCvpcL$eFL=06&8tM8DU&JByL3vQ=)q?wRd*{ibKu(@~mC2E$QmipLJevuT!_Z_;d%
zj!fZwmgMFn9T+!1JI<fZQqy!Fn9J6<$ATWoUt$~*MDD}sbX25j;MdY2i~yrcZo#?s
zCfpdtBK2C8J4<KGk0GYVZ-g~&F$LW6O|0se{Su>umjNTf4Zv1R7WQyFgKL`d=d7*@
zzmXiz^QB8>7&dX!^~}x44JW6`@i0$MjJbt4lealTeXt?LHW%lRA$$q5l+w$5fzc~~
zo7<5~XLCSfwqR^SYQ?jKp(jFC@Y*&rgS#;vrVGQ$+GS-eiAZJnsaeBdqu8!~V2+LB
zgMGsz!uCX1moA3$ykHSGWRvi4dq{PYw!^3f0JS0#xwBj5=%=IMm=lfa@CuwZ_nVTC
z^Cp5)>38^*iLR$;U$|6sg?OG#jX~4k@l4_Y?K-UX570rW!8LK}8a(Q+ZYaFiV$OIQ
z_*EF)Q6S4o8PsjOfv6VEw_04^RGsBzxW2ZmEG2xsw6_xEGOeaNCg@-vNa8yDZs0?C
zmDIAJ)t5p?dcF^%FR=(t(js;+q($rkwm4xAutWG7;Nf26X2~#17dhN|&(#FliQMTd
zn@$J)VV22#VJJ&i51ej!;lwIcTYutmw?KQ%%2V}hy6C^ic?6{fi@wdHud3<t7?X}t
zg%i~WF(35vWsBEZib7j`8TNG;)$9!*)$A@{Orh=pHbetGJY}~c%C!gUfUKBl6Y1?N
z9TXQNm#c)hBQvAA4iI5w>&ktE)aZ4zkXG6Wm2T}s9D>n{f}7TZt9)3%efV18TR>Xj
z+kj`B@D5;S!_D_i(Ps!OZB8EFp4<Wt<TmRk3rs97wCX<D3Jg6)Z`3vfzDfdQxwVrj
zD2ag?HJ;%e*l%Gx4B!0$sMeoln;l5_;=x?mWmL(WHJx7n?NZ<U8vBdHmyw~+N`_*-
z2Xd<R`#`Gp1HiLJxtLsp+8_J782BFM2u2!OH9b-q_$aIg8qYAt!&n$Ddq0Ti5v-c+
zU2*Diu-8^yRR5PFBQ?{7FziF!x60MU;3`$p*Z^Tl@+^pTE-^#uOyQS}uoOMI*O7x-
zdc4>r`~*;=q^hzWBB)JV$cMnEFkR7DxAsRME#@bI_}0qvvs`_7mQ0GT;d8`lR|oy`
zz*K!qVhvi&9{gWmUi@{B>3sb+xl`s($72MF41WN5Jq6glA{+$th_!{feDvktncBZ7
zf#C0$^J@e4O_;wzD>Xwa{f(jLp+NN!B)Rj8Gci&-uUw9F?JkD?gb5s&LmQ?%oeyQg
zy0zxNUx8Jh?W!LWBsLv(*KI)ASl!pIT(rsL#1#F9v7=CrhffCKsKlX<^{f8{CTUlF
z38Y>16`&l}Vrk~&ab>!HFxr#7leOy~g9VebkFV;*e1MtCf#Db~*?d%r@>n8rMn9kF
STFnZzDrD@(laq(|@BLpra__?c

literal 2980
zcma)8%Z?jW5UtxiV>=le!Xi$aO`1$*CQ1Ux3XefN1c(e14T3BPEUh-~(Kz@;cL$sW
z{6zNP1zGbF3-}BEh&reG#b8Tm$+u6{ty}lh<KFgs5=XPs@g$b~apUP?o@DZMoXp~h
z<kF{6CZqUNy!6p9d%TFH<$WL*op=uv-Pd0v9vt}Ihx7R)ch$t(Q6TgI{R`fbwr&?<
z1A~L>t<rZAFX$grbdR@>J+9LQ#9}3O_2~TqwS*S|eZn2Uc7rV3z3Bp?wDjjW+ZA#%
z8m8IWEfY*jqvajTuJ4U!XVGw+#UqjH(9?N`7AAuYDR#Iyr-bl1SQ(|~xq#YBfLHc>
zFJ7d8B0UVQsj=eeVd@(tt9WaVp21xt#1LR$WSt_iwrVu8>`b;W+04r|sF<U0d{8$$
zn%HAatQRlGX_m8SG_^>0SRPWn!m&%ODF7`Z61ja)_!z{K@sx&Qd3X^*hxKMktn`;z
zG44QZA66RrcX;bc@7PdZ$(8&yk}R2vRBJ=}4Y9^;W3-m43KT*a6dAg#LOnzG2b<ds
z3)^(x*aLnE1G(BB%tHvJ6`Avvl50@5X(nagT~%FuZ{1nrdAPRoA~=wC%Nr7OQ6-Xq
z6A3ClOums?r*ze#L##AQGG~g6IgO0@KCId_H~{Pt-T?gMhVLz+aS|^xi1jwCWo6&@
z&KAjhemWQ@iC!VX3<h=vtqXFYVfpFUt5K8)_FGP$vW?^A;8~6+C^Z??&8j~F+a7b}
zx%vvyE(5y_Xi0b($dd31V1ov)0yZ@$J0L{^LQ6NJZ9s<LfO^`lNqm}Lf~-y%*)5&-
z>wzJvjSZ-G4jiIm(FoQN-Kw6weV<bp>@r{#P9Pc|2JjkWi|}<Ii|`G=lm>4Cc6YqA
zFSTx2+hUJkdZH)&eZ8>;(Gp^QX_a?IuVNTt_8MiL4a$}h%sAGHnW9o1L(Qlq1Pt~u
zvfDx+n*9J&Yq+9s?x_0w@!Hrn$8aKP%d;!KQ{=Z_V}G9bIx<YOkzq35p<lvx0WI6_
z0jAAjGrilaKl%rl_#VR{2EFx`c*~*Dz{S5^(RhNX5QD?OZQrVr7(!V#+uJJC)4^Wb
zblv<v9SNyPfW)vO%)NdJbI~?~XjDmK2ZWiDCsndmsuNPDi*VfxLkX*(nZOVW1H!w2
z*2G6Zme!8}t%(_ceQxeS8)%NLv_Aq_Fh428_f(&s^)AbjXqJERo<e8)vr{RrDyAmG
zh%s0+ycB<d^4XV%Fz52$^iD}1Pp44i9{vCd?G&JVxq1b}H6c((sq2Sb|FYEnhExQ9
zht01=BmK1p@ha-lB4l`fL;17{&txdM&FZ`*W@@LEn~|(zV*kWEl`A0nuy!fV=0~dD
zc253#sc-u9mfaY^opjk-HvzS*R@FeS*=RPBy!$YBSj7`UCWGprG@u)@n;rmKH+=zQ
z-Sj1(9@2bMdV2^R9sL7zqBYZ9>mPw{c{td=FW7~A2bQ*oYHmy(M@2e5R|7qppDk>!
RR*Bjr5_fktI>JBme*rr;?JNKQ

diff --git a/src/builtin/obj/sum.olean b/src/builtin/obj/sum.olean
index c3b3bb84574a54f0da0c8d87347bd56798c89bf4..adc566891cad4858663c9d3da5b395f9b2de9b42 100644
GIT binary patch
literal 8857
zcmaJ{TWp+16`q;(E#52y41J=JT03!?5ZZO!G;Kxr6DO4sv<=XU=mX0-UdQXKcb(l$
z>Zs)b9s)?bAhoEp2q7*lAQi#`5Xw!h(-frOR5+x8L?u#+3A8E?rcD|UaK7*S|39-E
zo0azLnKNh3oH@6-*tJTjSe+<WN+$l;^7Krt-ZcA4^=heN;?~{8W`Z^jj5QC<l#*s`
zrdh64ixo3onlP?$V7f3<FO8cXx83ww<L(n|hl=iTGiH@5n*NMS2N@@Q7X6uw+fl1k
zjOj*;Bt<i5E7}39V_n8oOZ$Nu(<u$${b*PSb6xzASvveQ)mk-PV0IlidjT?CfF{SW
z?*!_SHBfy}y!LESx12}cL3AJ^>sF(%-7%m#vjLq<t~qHsU>sAfR=k18&?6=xPiiQt
z_&(6G?C2cGaOJ&?+H|rEbU3ehZk3w_$*cy*P|tS*Rm1fG%aQsXphi@#)|!QKwOOwj
z<89LEQA)ZV%xjdWHU@zf=obs4(HnW|=DOY8pqZPpaElEG!VsAObY2IL2gv#r<k!QK
z(=(wqG-DrmHiMnEyhRurho+}NkN^O<1z;;cP8L=#O-LBw!|}If-DsgPS$oLXjGHJ{
z8YP(`<BDUA1NHG_HqODo>F_E>kdbE>!-H*^L6<#VZZyl)Jxwqf69I5dxesFz@_Cnh
zt%c{&T2rppuk!p3^dQK__?x4>yyqQPx5jHk1LRhL`5FNFXf^#xHPzeXSCj&CBy1$k
z$Zz-Z8V;t3!~DPu_W<-IZvCXX6|_z30k?ReLue0sNi@bL5Ow}LfRgD!hV@$J_%;go
z5c=pv<=ut0MhLLfq}NNsnb4+_#j#45t)nO}<*Ja&O({eC<kHNdc6&8FX}dVXXu%uE
zOmrjANuuv3Rbnm`S}0Y@arAK^bjrSN_YgU=>!k1`<skl*JWCbw&Z8|>(>HWE*Xxi5
zvl3d3Bsn2<e|MbT`)Mw+N9afj1aO~LIW(E```2ZFBNUVH1m=<$-5`yY7!^J1p*?qi
z9T7Up-^tj5Xp{le0<_dH+8TCrrJ`FvoMf;_rHONx3Vtpznd72n+AK5FW|=HyG$7+J
z=cD}&w;6;+%yoimm;z`OH4}%bK@dpGM%c|lmI%W}&;b@n+m`q$f@pk1p*2NyZUd@o
zz8#pBTSmQEuQlUFDLQez81Sp}%B@r7;1sc}l(IB#!eCI7gC)%i)IQsy^zu#|!zeA^
zpQX}FJXJbkAF12PMSDLEba$JwjQEeKvM^W@24s5@ZE~dQZ6hU2+lnk`YS}m|(u2my
zwnzt?EH+4bxtH=8c4U%N!(1%<S}i!Omare7OQQi;P}d^10UTF50#t3V)1$k9D#M*X
zv)yhqK6U&ERWP6IZeFPfe0i$M+1aMI@@h*T;k58}4)w{L?<9c{>&G&!o~6_$FhN8n
zTG=z@No24c1=G)<;!vxKFis~rBd_8d+Eg(LRb-Z1^pWAXSCs82P}EBp0so6$(K)Xu
zndppY0}o3`gMRSu1vs|yAk_^_Cz2ZY61n4Gz@oa)J?9s-fHr5F3l`PM`M4-Doc4=i
zdoEa%O5gzQ{M7$thz<6#V`#r1M~Rtwtu|38*Xwd#=I15A-vgY;%5h|-;Lk!JzT7@j
z1nQpvILFzILAhX}piBGCcvCHS`%>QsOw{yMU}woW3pD6%BdV3eC(U}X+5oRHr_^Xb
zsm>W-6nPQYAC~Jri=K-tT(1E=1@L;COCk`dpvqvyB<CCGc^yDA7+8+3UmKqxL1(sd
zd=wYdUa2CbJ<amLa`O<z7_$VRJgQAU2=w|A?Zxa;t}Yumf~1JtJP0lLWPJ-F2rl~-
zvVBQJpz{*I+W=Pp{>_<~jmkF2AeqV+_SC9->tGRqT+T;{5~w6<z@S?I^$Mw%1=DK{
z<p)8iYJoGYwmYQJVdc|u^jxXljxhwVqm603Mdb}{1kY%ZMF|f#OzzpXua&6hR~|7b
zl^)a@dN0Rw$@h8mexSNhJ^<9EMb=)^Qe@G26yc;(Mri94J{q3|@#nPH2+*4Wv~WHJ
zGy>2<$?B=&y{k|-?X@k16C+rhblN$zBLF>&JP!0lfZuRhrtmLFgsz6u>L5<TX(ROH
z8AvCAYB>v7LHw0`?Vyj4xaOhjls5w-g!1DJ2K}0|(8oF-@yeC<2N84(oCDPNJo-_*
zEDpeSaQWheu6D_h5IM8m%(L@i(l%PKxI9(YTOu{5#d*<grVd}iNWU=MtJ;WaJuNir
z!B0n|#Y)9(6}r`1N?SMb+ivx#j1pw;SkA1Gmys4L`$4h`Sg}~4FIWOqe6x+{r`L^$
zbx8+x8QrT`hn6tz0svG0LNHEfc0`!*yORw8WV3hD%B(=A*%Mcwp_U2+_R~5SD-Pze
zBcQVE*pC49a|b~Kq1uy{olgj*wd|xfWIP7(lU~G<M-M4BW9-p80Bi0uApB6i_PtDi
z0vU*Y+M`9FT3aYVBQm(;hGO(p!WQG2f}zg=Jb!hz3)K$zpwjFHk<ob~$XgH@>?eTT
z1fYk%^Md*`THy=;o>%32b;6+MB7k-S`<s02?cVjey@I%6fM2~ELl8Dvy9wAo09c@t
zjTVIXI?lDSj=$Aqg={nWbJrjmVB~&iwGXtrK+^!(1(adS1WyCxQ$lvZt~6fWGg)ia
zrVlN952zZ3a2diJ0G@VgvUkdlUXVeQC3MSnMZ_yj*K^Pj2(h0*zw9kxsBv{EV;pLe
zVAOL4CsuSyX!hZ(ob%*GLF0gd8a|_RS-JOP@Qrfb!>`<$0KNl|1BhSIfa=Sm{UY$b
zWZdq;awFwvR;$M^4t{|{GM$XIUx0+e0G|iol85C1MBet$Huh1j{}FG6d}1yQRa)UF
zSc6+rgf?~NZmH%IJFEGEo0K2ezAfiOiPALWhz@>Je>97y+X5d9Z9h663m3&>hb~Gt
zbBt$<KFEv=UYoXSKz<V(BUechqWu=ShB=P4yA#Ck0X&TtWW0V(O!&7P`(1X)^Gmf<
zXnkL_PooR{aU@FBm@V)z)_TiEiDh-mqGgYF1xrfzr}zqY9RzBM$gK5JqgFXsl0%8N
z$o6n}T8Z@FGa`fSkNsn0l1mV3BKcZ+CntqJeoykxR&$9j_0mLDPlt0|!Lkf*rcC4o
zH1$45t=VR_+aR_U5(_No5-5au6bNA#ug4@Z%y^U0Fk417dyKPVpoW>3#?kWVtdS{W
zM~T_z88mCvJF$jN#`nY;+WAmJ^dO<_ya2P5YG`>r!yI<r`*|suP8nf5i!+lBq=p=*
z(sB}OlE8du*Mq-3gAu3N&sI<%-uGEmp^N1mjtODUr7nrp1pk8Hyj4X*_s~FCl|6TZ
z+&qfqdTF*PkI%I!3=*+`xH;HY0R9YcUVw=Ja;loVSI5P!w_P{b#r}m3K?SmlUN?5p
zy6u+82D+Z)0O+cVfxGPDps%2X^rg%$qVKPC%2Pmf1`5D=IuM}uO`H`22V|w>$o*S9
zkS>Q~%diif*RC?Gr>@V38sP%PFbTax-phXZ=~${|-`pUw%xe(%wl^0piWa9iJ0IA@
zUr*!7R~*Hoq)RKCrM&-w{XYWIi!-!hQrV?$&<~>>2dy{3YS@AHXBWNZGD3450!)t6
zGz7C)o9h8F0?^zeCV8iSU$bAqfhw-=(q+HR;amEFKL((sl(zW3ZwvPSO6wf;e*|1D
z6^n^-M5y*T%wvDTD1lSWaorz&3LMumcP-7qZ3Q*gtwoO;6kvY|w7qzN79W0oO>6ng
zVnz5J7^L(R@r%);#N0q!dW2~I7$kp%d{^f^_|5^m;vXY4rr{VK!6l1<UI1uKUDbc5
zbj160lDd^7bunhqhu$LEnoOv{8fo<Yd@wySLSurZVUbpP1N_1GCpey_VIKNHC|&LY
z^u;Wh1gN<AG#OhI{3p1yBvUIy8h1H+l2czoe~>lObi+Yvq5EHf{(k)5Inu8`72<}a
z$FwDp+X~vP=t&O6j2fIDT}SL|*O5jU|2`L|6clIP&=anMfsedl9=UCTwdD;r0{?8Y
z7repoxLh4SAWvJh>axe<-9lx+*@q#yQ~p4cPe}2fRS`eth;$4|#~2!M2mSqIkE@b)
z6v?S)3Vn%zW8*_G92=uw6U2SI8||+Hy_e`WfZpGoh=Nb-ms6V=P26drhKbADi(dF(
zHN7gcobZUD2Z4z4sbX-T@<a6~ut3oO81Ej?$10doW(0@;Buz(42u0(Hg92B~cs**+
zJ}=NL5eES*lj@Uks*{tN#LqfRin0vSL=H|A^QpWvM$H1pQ(GU8j`adhRF3AOd4hG6
z{5n=VGI1Thg$UWXxB`uW^qk}l#w!5NJ|+~h*j1P?eS*dd5KQYc-^{R7H^l(I4X9U@
mHda-Wzc7API5P4WdC!bi%B?B3EyYZVt+u<W<9FiUQT_)ll9dbq

literal 9228
zcma)CZH$yx6~6b*eh*Vnj6WI-A>|vyGC-lIf!R{rVyu<4YHZ9n%g(y9%+4&c!&ei3
zSV%<w=uZ>+Vfs%=s#dFiq*~LYE>evlf-Z$3G!;_=m^Rgf0G{VL@B5y2J}_>=-E+@9
z=iKvs?|YYewOp!=SE^+f{rJk%biL7Zd&`Ylx$2_XqormH&g>s;9-c18)B1F?Qm>V&
zZmc}+!p#1u;&h`t<_1E+4S5%y5NKFM4}@tq7)tKGOh}kqkTs9>OePH1>s9CaF(XRB
z4CV^<0P0zm3AOS*fX?;G1n_;BcnAx9{3W~e*fzC#Eiy2>43t9{GJP0bj=b{$hS&zG
z4~%Kg8FkAUcn`s)8L?ZP!g<e9)tM9M<Z{gk*8}IcO08-RBEf*TgfxkxsNy2vvRqi6
z3Dc!Y1F&=R`okdwFlLr!=#-(E`c!No@WG7AQRxo@t6p3PNU<LQ=tTcoy;-c(nvJ@1
z=Ad2!=aCM>0!6CBfuK8<iMufw+HS7S^@m4+bL+E+kxw(iE19KOq@X;Ytm&K=lgs<2
zrqkMFK(mlE>j2WR4+!DR;i)MgBpWb1fZ;(5IWeqJ9+#ZL5Baxb!$@&vqJGf%Oc*a!
zXUeigCX_~J_BY1j-M9y{sK-<+Kt`TR%oWaM2Q_=FGSjTo_B27{oYDfyJpv=-=R@+(
zd!zwo3o5lnM;Z)c1sONW-#Plr(jY7cdI^Sk4CzM+Cc^^Lm9EhU6RB~hJOwE#$F(&?
zvmn~zy}+EEE*tFl1q=)00DnaT4BT3Z-fTiQ0K3T~G1O~;)crpNkVH>1+ZTHvwo$-#
zfQ+Zo?!;Vk1yJH#NDnUU-HFm@HC@Cb=sJ~}pes%3PW;Iw1xM{Bv}&2@QQ^_et4U07
z4ZsS)j}t4|mk2GEtCc7ZX$XT*?GFb@nO!FRDDD!`Z>hLMp~0xC>4|xa3`0+A1Ipo$
zq}WVcq>$N&J3)iaA~`cJ>KdS7x@@p?Nr|V?6weA?xGVz(<Z0w%qC=d(s|4MWz@mC1
z?cyYTM<}8aITe#h4C)lB!jNhvZpM;=TL4v<Kdc$eVjz#kUJSH!-yo1wo%U>Kb61u!
zSc}KF-$u|MYx9ztPSUPkqUcQ&O;gmX>Lnt&W#T5;NHP)UNDnrZLT|~#5|GX^53{}0
z@sj}65iAKU-%k^}T)WKu(x${Jv!1!CZIsbh6~VGx^+eFb^U?>CR7+=&h6E%@DQ%UB
zZ_&SdkVnC#z5fXHXXdH?nhC@{L@GM@c$?m-BsV>FtKM*9oH2~R^O$Qw#0j~bm~_!s
z#kR?=DOp+%ei!7dW!PO7r!Es>i1L}CT#`ZsDf|%S7`N31__GAb;z)Hxny+@y@Q2Ay
zaHoNv0T_s7m1O(FNOYC?1$yZE_>?rIC^%15xw~zYZ+9#GK1^0?21>OA8xM119vdlA
z=CVoM#I2qKeZgFB>v<xXq9;N03iQsm>J5+eVzFR)&tgso71DZhcaJp^oHp$_S6XU+
z+O$6ndL<>l$=+ew&zkmJXLJiIc~?Ujk#ho)PTieJ6$a56+x{Hsqr`!&eIS@MTjwz6
zezPfCd(Bo7TrgWXS6bS7!8W@9SxQQNl}(WM5ZabHN>73Q_j0G1Zq)1J#Y&?gw|M@X
z!}wPWXR>lHnl9R<49JUARkz3d64kRk3qW4RaAkF>AF<|ubr&(bWxkxV08nWPpt}DA
z<rPvs1u(VThEyj?(3*`>Z3eW?omZa%)GYx~<PAV?c3ZxJl^ZKDzK7vFhWFbdW(ul|
ztqJ7^B*%boN4Ep!#^UH&3p|5H0}D~d9+HMs-qWlcs5B3Q(Yc!#lt#6ogFTnb;Y!u#
zEhM)sBW{EEb{lbla(FR@H@!DoNq?tB7$_jc-2nvMy<T-$*UGShDKxphxTjwGdIQ9=
ztNimWr4{E`xx@XLk#k+vJ+||MpiJc|#Zi&u{MjKCJzjoVuF7}o>!aG&<vbl_rm(}O
zzF=O`X1*Q!rjBb~BmBLsNWE_lwIa1wKLMnM_lpL837{U+Uj`VGX6`@M(#)}V61k>Z
z7BHu}dQmx!`L8kj#ymHS`KuV<5x0@4dIF%bGyFUiRTAe(SN2O=x-!_<<WvDoKOj>I
zyn*>2Oab=TKLU9f!*5LiWj6&>A?DjzkZOCRuC~)_vf$TQ5=T80^ykerYy@PA4mYe{
z#PF7B#*TPNaDI?VF!PiNl&SneFZB9>a}`VIfF3F1*Zp4|5R~nEz*@g?wT$i>2G!2I
zqb8Vl5*K(x$7>+J3r;gukI6P<-YU3T$5V0JAhW|)+z7+Alnl&=ySbVcsf?{c#NOz4
zkQ`HVhi)AY=#&YJ&#gA3ZQp)^&GvP)5$j-VfA2!pyD14W^}9ORfc`AkFno@lXCWX@
z{H~~t<=fksyI>imZOu9u_V>Hm*MZzEgQI4tG-E<4GQONXE@Z83EO{Zo%NT!>&(HV;
zNUo=&T+z>*LBKCz___S^i&#8g!(3ZY$w0Dcui67_pcgdr+0oKs^i{@BL_G@huVeUK
zXU`C<Uqe5zNokJ&axECnFgRNCK(ZO10fetQzlB9{RX{7eyIeg$gA=^7u&}~oU6(Qa
zm;CbuON{eCz7OPG3!(Gq2M<nl&-VFmOtTnr99teCXa>D_yUz=WAJSisufSvgT$(^!
z!+_{VeP|~@<}({Xa?TY69a5*<SY^*dy;+|+-1YmV<`~dP2xC3sX{+Ag)15vHU`0&m
zm(LmkrZhuOrk5eaAH}+yRq0f-906gJY84P_s&Qil_k!T*tXwbU9YrrcOw{z_QJ<IB
z4lv&@*G&9&?uQtDgn?g9(JLb6`V8y82Us2<l<%=(H%_?+)*I0~iy62<wi8~@{&@^y
zzKww<Z<1#pdE3O?`Qx<z2*;zq<YRZ~_Z7Wx5(}xXJr*l<=9iDUPyDRzOML+vWBW0m
z6D7)1kSjXaCE<7$@7P5?n0hoH|4iB_USrfKy&Qm_+4&?ZGWEtbtO-dU@92;O$@Kgt
z^0CMF0{IgRFXA~JufOBt_JZYq%q4kts+Eha@2mbrEMYy$MClrbihO?d=Gj8*Sv}h5
z+0%U~ll0hx6#dF%^PR;!C%ZPvGxh3$vNRO)$Z(oH=|p;w+97=YSN0ei*AnFM!sO|~
zoE!$xJDNS#&Bn3R4>+oNA>L~c0^lr`cy#MtggI+k&p(*0pOc*PWbmmpn~R+>r`C{u
zvP}q=_=Qi&%s75QX~uQY(({T&tu^CJC34IAyC$jdju7&vqVC2(MH-?`1|kjp*|dgO
zfdf2S{LMr|k9!pB*q^1OqnO`}w^Ks+(f@@DV5Ej*RB1U$JE>*<%|ZGYC@x`mv;AVG
z5ny_-`9c@ZZ%5XKf1BP!NFp@_a`p-0uSBn;{t6i>Xg;aQ$T=MsR_UKv%7>crG+$?Y
zWG9GYdw&N^IL-V&fYZL9+RAHw`~cFfF0Y)|=mGR6f8EsO5*^;|9KDt=0sXb)%ItC7
z^w-RQbBO_Jd3J?0-J(7faz_j|7`zhzbzAa2k2!;jyzn28h-xa4AYE3vl)My3q!Js+
zJBjRIklXFJ1zAA4d|D%X!|B_lJ%o7B2EDB?gb6Rz@^_L`K4cOfh76c`WbkL%(cq|{
zx1aA2<Y11vWsXv{x{10YOiusCf)1&hz`nqc#`gk<VnzB}jLf$%zeUHT9)#w>IrJ%)
z7~gOYgdz2$#bLy$qz+h!sU{SlxOzwQkCy&fT+E_#LYDmrvTufg{uvC~l4;dXZ7$IN
zYSFXQ{~Mrc>3m)g{+Af|Am#bxs(&#(t>?@u;JGaS!b-a1Rm^8GUj-<vkiowOu)XsE
z7hR%WPlBSY6h`|$gFyOL3BSQTLMVJ9>RW>Je@k_aD(O0#2I$_#@J^B-TK|7fcGbK`
zocwO6?RmkxB9N7Pz~zu17aEg%T<+Dl+_8Q=Nhg0DbFDSBa;*a9fn}=J@q4BSbCN_?
z>AC+<s7ZQ`l1R^jHF}h8c#z5W6p3Wev^$$rZHuaGWZL7YAIgm<s6U6T17e>pFHG$l
zQdfEtmj-w*^qD0lj!$cB&?YWy6Y`D{dkDB;taOxEm>*?An6Cu}(giX^1qTyYRg6xU
zpHvmAEIcC1ZB^wj0he6DCuEYogjZ@~`{lK+Uh8@Ze@w7UNB=aW^bUlP^)V{?<24-O
zUY3QtER13jEik+<41^kSC)t~jT+#axsyMo8KWiWYAHK>m{Q<xt!509Q`eRY(kpBCK
zL3~jV&~cwsS)T_|KP%xi{cvZW;WN3i7AU`t_0+Y^SoM~ncODRdKaA=V8(bMbYyy%Z
z9w{FJ6skzAyY>UU#n3-*&@BZrVd&BbW<cl`^SZ1?=ralLA^ba|)^+N#!t;%R;W1CI
z&v7TTtaLse#2oATx7ef&M|Mn`9e2Hr(T+bs#C{0tyn=;qMizkP0FO6T@j*6`dj%UA
z0CsAv3S+jP3C`2WR6PPhRW*KmI4+osJfVJmn(6AcCeZc-atSogKU^EziT?rgUrIoy
A$N&HU

diff --git a/src/builtin/subtype.lean b/src/builtin/subtype.lean
index 38dc8481d..505b92b69 100644
--- a/src/builtin/subtype.lean
+++ b/src/builtin/subtype.lean
@@ -14,7 +14,7 @@ definition abst {A : (Type U)} {P : A → Bool} (r : A) (H : inhabited (subtype
 
 theorem subtype_inhabited {A : (Type U)} {P : A → Bool} (H : ∃ x, P x) : inhabited (subtype A P)
 := obtain (w : A) (Hw : P w), from H,
-     inhabited_intro (tuple (subtype A P) : w, Hw)
+     inhabited_intro (pair w Hw)
 
 theorem P_rep {A : (Type U)} {P : A → Bool} (a : subtype A P) : P (rep a)
 := proj2 a
@@ -23,7 +23,7 @@ theorem rep_inj {A : (Type U)} {P : A → Bool} {a b : subtype A P} (H : rep a =
 := pairext _ _ H (hproof_irrel (proj2 a) (proj2 b))
 
 theorem ex_abst {A : (Type U)} {P : A → Bool} {r : A} (H : P r) : ∃ a, rep a = r
-:= exists_intro (tuple (subtype A P) : r, H) (refl r)
+:= exists_intro (pair r H) (refl r)
 
 theorem abst_rep {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) (a : subtype A P)
                  : abst (rep a) H = a
@@ -33,7 +33,7 @@ theorem abst_rep {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) (
 
 theorem rep_abst {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) : ∀ r, P r → rep (abst r H) = r
 := take r, assume Hl : P r,
-     @eps_ax (subtype A P) H (λ x, rep x = r) (tuple (subtype A P) : r, Hl) (refl r)
+     @eps_ax (subtype A P) H (λ x, rep x = r) (pair r Hl) (refl r)
 
 theorem abst_inj {A : (Type U)} {P : A → Bool} (H : inhabited (subtype A P)) {r r' : A} :
                  P r → P r' → abst r H = abst r' H → r = r'
diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp
index 79b3eee8d..0c642e214 100644
--- a/src/frontends/lean/parser_expr.cpp
+++ b/src/frontends/lean/parser_expr.cpp
@@ -861,61 +861,26 @@ expr parser_imp::parse_type(bool level_expected) {
     }
 }
 
-expr parser_imp::parse_tuple() {
+expr parser_imp::parse_pair() {
     auto p = pos();
     next();
     buffer<expr> args;
-    expr first = parse_expr();
+    expr first  = parse_expr(g_app_precedence);
+    expr second = parse_expr(g_app_precedence);
     expr type;
     if (curr_is_colon()) {
         next();
-        type = first;
-        args.push_back(parse_expr());
+        type = parse_expr();
     } else {
-        args.push_back(first);
         type = save(mk_placeholder(), p);
     }
-    while (curr_is_comma()) {
-        next();
-        args.push_back(parse_expr());
-    }
-    unsigned num = args.size();
-    if (num < 2)
-        throw parser_error("invalid tuple/pair, it must have at least two arguments", p);
-    if (num == 2) {
-        return save(mk_pair(args[num-2], args[num-1], type), p);
-    } else {
-        expr r = save(mk_pair(args[num-2], args[num-1], save(mk_placeholder(), p)), p);
-        unsigned i = num-2;
-        while (true) {
-            lean_assert(i > 0);
-            --i;
-            if (i == 0) {
-                return save(mk_pair(args[0], r, type), p);
-            } else {
-                r = save(mk_pair(args[i], r, save(mk_placeholder(), p)), p);
-            }
-        }
-    }
+    return save(mk_pair(first, second, type), p);
 }
 
 expr parser_imp::parse_proj(bool first) {
     auto p = pos();
     next();
-    unsigned i = 0;
-    if (curr() == scanner::token::IntVal) {
-        i = parse_unsigned("invalid tuple/pair projection, index does not fit in a machine integer");
-        if (i == 0)
-            throw parser_error("invalid tuple/pair projection, optional index must be >= 1", p);
-        if (i > LEAN_MAX_PROJECTION)
-            throw parser_error(sstream() << "invalid tuple/pair projection, optional index is >= "
-                               << LEAN_MAX_PROJECTION << " (internal limit)", p);
-    }
     expr t = parse_expr(g_app_precedence);
-    while (i > 0) {
-        --i;
-        t = save(mk_proj2(t), p);
-    }
     if (first)
         return save(mk_proj1(t), p);
     else
@@ -1069,7 +1034,7 @@ expr parser_imp::parse_nud() {
     case scanner::token::Show:        return parse_show_expr();
     case scanner::token::Have:        return parse_have_expr();
     case scanner::token::By:          return parse_by_expr();
-    case scanner::token::Tuple:       return parse_tuple();
+    case scanner::token::Pair:        return parse_pair();
     case scanner::token::Proj1:       return parse_proj(true);
     case scanner::token::Proj2:       return parse_proj(false);
     default:
diff --git a/src/frontends/lean/parser_imp.h b/src/frontends/lean/parser_imp.h
index 9fe083ab9..5d0533238 100644
--- a/src/frontends/lean/parser_imp.h
+++ b/src/frontends/lean/parser_imp.h
@@ -326,7 +326,7 @@ private:
     expr parse_exists();
     expr parse_let();
     expr parse_type(bool level_expected);
-    expr parse_tuple();
+    expr parse_pair();
     expr parse_proj(bool first);
     tactic parse_tactic_macro(name tac_id, pos_info const & p);
     expr parse_show_expr();
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index c29d1b2cc..711deccd8 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -76,7 +76,7 @@ static format g_ellipsis_n_fmt= highlight(format("\u2026"));
 static format g_ellipsis_fmt  = highlight(format("..."));
 static format g_let_fmt       = highlight_keyword(format("let"));
 static format g_in_fmt        = highlight_keyword(format("in"));
-static format g_tuple_fmt     = highlight_keyword(format("tuple"));
+static format g_pair_fmt      = highlight_keyword(format("pair"));
 static format g_proj1_fmt     = highlight_keyword(format("proj1"));
 static format g_proj2_fmt     = highlight_keyword(format("proj2"));
 static format g_assign_fmt    = highlight_keyword(format(":="));
@@ -1120,33 +1120,24 @@ class pp_fn {
         }
     }
 
-    result pp_tuple(expr a, unsigned depth) {
+    result pp_pair(expr a, unsigned depth) {
         buffer<expr> args;
-        args.push_back(pair_first(a));
-        expr t = pair_type(a);
-        bool cartesian = is_cartesian(t);
-        while (is_dep_pair(pair_second(a)) && !has_metavar(pair_second(a))) {
-            a = pair_second(a);
-            if (!is_cartesian(pair_type(a)))
-                cartesian = false;
-            args.push_back(pair_first(a));
-        }
-        args.push_back(pair_second(a));
-        unsigned indent   = 6;
-        format r_format   = g_tuple_fmt;
+        unsigned indent   = 5;
+        format r_format   = g_pair_fmt;
         unsigned r_weight = 1;
-        if (!cartesian) {
+
+        auto f_r = pp_child(pair_first(a), depth);
+        auto s_r = pp_child(pair_second(a), depth);
+        r_format += nest(indent, compose(line(), f_r.first));
+        r_format += nest(indent, compose(line(), s_r.first));
+        r_weight += f_r.second + s_r.second;
+
+        expr t = pair_type(a);
+        if (!is_cartesian(t)) {
             auto t_r = pp_child(t, depth);
-            r_format += nest(indent, compose(line(), format{t_r.first, space(), colon()}));
+            r_format += nest(indent, compose(line(), format{colon(), space(), t_r.first}));
             r_weight += t_r.second;
         }
-        for (unsigned i = 0; i < args.size(); i++) {
-            auto arg_r = pp_child(args[i], depth);
-            if (i > 0)
-                r_format += comma();
-            r_format += nest(indent, compose(line(), arg_r.first));
-            r_weight += arg_r.second;
-        }
         return result(group(r_format), r_weight);
     }
 
@@ -1211,7 +1202,7 @@ class pp_fn {
                 case expr_kind::Let:        r = pp_let(e, depth);         break;
                 case expr_kind::MetaVar:    r = pp_metavar(e, depth);     break;
                 case expr_kind::HEq:        r = pp_heq(e, depth);         break;
-                case expr_kind::Pair:       r = pp_tuple(e, depth);       break;
+                case expr_kind::Pair:       r = pp_pair(e, depth);        break;
                 case expr_kind::Proj:       r = pp_proj(e, depth);        break;
                 }
             }
diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp
index dc0a06698..3f72b73c8 100644
--- a/src/frontends/lean/scanner.cpp
+++ b/src/frontends/lean/scanner.cpp
@@ -32,7 +32,7 @@ static name g_have_name("have");
 static name g_show_name("show");
 static name g_by_name("by");
 static name g_sig_name("sig");
-static name g_tuple_name("tuple");
+static name g_pair_name("pair");
 static name g_proj1_name("proj1");
 static name g_proj2_name("proj2");
 static name g_cartesian_product_unicode("\u2A2F");
@@ -215,8 +215,8 @@ scanner::token scanner::read_a_symbol() {
                 return token::In;
             } else if (m_name_val == g_sig_name) {
                 return token::Sig;
-            } else if (m_name_val == g_tuple_name) {
-                return token::Tuple;
+            } else if (m_name_val == g_pair_name) {
+                return token::Pair;
             } else if (m_name_val == g_proj1_name) {
                 return token::Proj1;
             } else if (m_name_val == g_proj2_name) {
@@ -471,7 +471,7 @@ std::ostream & operator<<(std::ostream & out, scanner::token const & t) {
     case scanner::token::Sig:               out << "sig"; break;
     case scanner::token::Proj1:             out << "proj1"; break;
     case scanner::token::Proj2:             out << "proj2"; break;
-    case scanner::token::Tuple:             out << "tuple"; break;
+    case scanner::token::Pair:              out << "pair"; break;
     case scanner::token::Placeholder:       out << "_"; break;
     case scanner::token::ScriptBlock:       out << "Script"; break;
     case scanner::token::CartesianProduct:  out << "#"; break;
diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h
index 1c5e0af23..1698e9704 100644
--- a/src/frontends/lean/scanner.h
+++ b/src/frontends/lean/scanner.h
@@ -20,7 +20,7 @@ class scanner {
 public:
     enum class token {
         LeftParen, RightParen, LeftCurlyBracket, RightCurlyBracket, Colon, Comma, Period, Lambda, Pi, Arrow,
-        HEq, Sig, Tuple, Proj1, Proj2, Let, In, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Assign, Type, Placeholder,
+        HEq, Sig, Pair, Proj1, Proj2, Let, In, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Assign, Type, Placeholder,
         Have, Show, By, ScriptBlock, Ellipsis, CartesianProduct, Eof
     };
 protected:
diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp
index e6c39a7f2..a6ef1fbd8 100644
--- a/src/kernel/kernel_decls.cpp
+++ b/src/kernel/kernel_decls.cpp
@@ -167,7 +167,6 @@ MK_CONSTANT(allext_fn, name("allext"));
 MK_CONSTANT(proj1_congr_fn, name("proj1_congr"));
 MK_CONSTANT(proj2_congr_fn, name("proj2_congr"));
 MK_CONSTANT(hproj2_congr_fn, name("hproj2_congr"));
-MK_CONSTANT(pair_fn, name("pair"));
 MK_CONSTANT(funext_fn, name("funext"));
 MK_CONSTANT(eta_fn, name("eta"));
 MK_CONSTANT(eps_fn, name("eps"));
diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h
index 5fbcfa725..0320f9c56 100644
--- a/src/kernel/kernel_decls.h
+++ b/src/kernel/kernel_decls.h
@@ -485,10 +485,6 @@ inline expr mk_proj2_congr_th(expr const & e1, expr const & e2, expr const & e3,
 expr mk_hproj2_congr_fn();
 bool is_hproj2_congr_fn(expr const & e);
 inline expr mk_hproj2_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_hproj2_congr_fn(), e1, e2, e3, e4, e5}); }
-expr mk_pair_fn();
-bool is_pair_fn(expr const & e);
-inline bool is_pair(expr const & e) { return is_app(e) && is_pair_fn(arg(e, 0)) && num_args(e) == 5; }
-inline expr mk_pair(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_pair_fn(), e1, e2, e3, e4}); }
 expr mk_funext_fn();
 bool is_funext_fn(expr const & e);
 inline expr mk_funext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_funext_fn(), e1, e2, e3, e4, e5}); }
diff --git a/tests/lean/sig2.lean b/tests/lean/sig2.lean
index 8a5da6021..eb46009b6 100644
--- a/tests/lean/sig2.lean
+++ b/tests/lean/sig2.lean
@@ -1,14 +1,14 @@
 check sig x : Nat, x > 0
-check tuple 10, 20
-check tuple 10, true
-check tuple true, 20
-check tuple Bool # Nat : true, 20
-check tuple true, true
-check tuple Bool ⨯ Bool : true, true
+check pair 10 20
+check pair 10 true
+check pair true 20
+check pair true 20 : Bool # Nat
+check pair true true
+check pair true true : Bool ⨯ Bool
 variable a : Nat
 axiom Ha : 1 ≤ a
 definition NZ : Type := sig x : Nat, 1 ≤ x
 check NZ
-check tuple NZ : a, Ha
-check tuple Nat # Nat : true, 20
-check tuple Bool # Bool : true, 20
+check pair a Ha : NZ
+check pair true 20 : Nat # Nat
+check pair true 20 : Bool # Bool
diff --git a/tests/lean/sig2.lean.expected.out b/tests/lean/sig2.lean.expected.out
index b50cf66ab..591cfd393 100644
--- a/tests/lean/sig2.lean.expected.out
+++ b/tests/lean/sig2.lean.expected.out
@@ -1,25 +1,25 @@
   Set: pp::colors
   Set: pp::unicode
 sig x : ℕ, x > 0 : Type
-tuple 10, 20 : ℕ ⨯ ℕ
-tuple 10, ⊤ : ℕ ⨯ Bool
-tuple ⊤, 20 : Bool ⨯ ℕ
-tuple ⊤, 20 : Bool ⨯ ℕ
-tuple ⊤, ⊤ : Bool ⨯ Bool
-tuple ⊤, ⊤ : Bool ⨯ Bool
+pair 10 20 : ℕ ⨯ ℕ
+pair 10 ⊤ : ℕ ⨯ Bool
+pair ⊤ 20 : Bool ⨯ ℕ
+pair ⊤ 20 : Bool ⨯ ℕ
+pair ⊤ ⊤ : Bool ⨯ Bool
+pair ⊤ ⊤ : Bool ⨯ Bool
   Assumed: a
   Assumed: Ha
   Defined: NZ
 NZ : Type
-tuple NZ : a, Ha : sig x : ℕ, 1 ≤ x
+pair a Ha : NZ : sig x : ℕ, 1 ≤ x
 sig2.lean:13:6: error: type mismatch in the 1st argument of the pair
-    tuple ⊤, 20
+    pair ⊤ 20
 Pair type:
     ℕ ⨯ ℕ
 Argument type:
     Bool
 sig2.lean:14:6: error: type mismatch in the 2nd argument of the pair
-    tuple ⊤, 20
+    pair ⊤ 20
 Pair type:
     Bool ⨯ Bool
 Argument type:
diff --git a/tests/lean/sig3.lean b/tests/lean/sig3.lean
index c3a9efe60..aad7d50c8 100644
--- a/tests/lean/sig3.lean
+++ b/tests/lean/sig3.lean
@@ -1,3 +1,3 @@
-check tuple 10, 20
-check tuple 10, 20, 30
-check tuple 10, true, (λ x : Nat, x > 10)
+check pair 10 20
+check pair 10 (pair 20 30)
+check pair 10 (pair true (λ x : Nat, x > 10))
diff --git a/tests/lean/sig3.lean.expected.out b/tests/lean/sig3.lean.expected.out
index bddad43a8..4810f0cd5 100644
--- a/tests/lean/sig3.lean.expected.out
+++ b/tests/lean/sig3.lean.expected.out
@@ -1,5 +1,5 @@
   Set: pp::colors
   Set: pp::unicode
-tuple 10, 20 : ℕ ⨯ ℕ
-tuple 10, 20, 30 : ℕ ⨯ ℕ ⨯ ℕ
-tuple 10, ⊤, (λ x : ℕ, x > 10) : ℕ ⨯ Bool ⨯ (ℕ → Bool)
+pair 10 20 : ℕ ⨯ ℕ
+pair 10 (pair 20 30) : ℕ ⨯ ℕ ⨯ ℕ
+pair 10 (pair ⊤ (λ x : ℕ, x > 10)) : ℕ ⨯ Bool ⨯ (ℕ → Bool)
diff --git a/tests/lean/sig4.lean b/tests/lean/sig4.lean
index 1f328c8f5..b83273d33 100644
--- a/tests/lean/sig4.lean
+++ b/tests/lean/sig4.lean
@@ -1,10 +1,10 @@
-check proj1 (tuple 10, 20)
-eval proj1 (tuple 10, 20)
-eval proj2 (tuple 10, 20)
-eval proj2 (tuple 10, 20, 30)
-eval proj1 1 (tuple 10, 20, 30, 40)
-eval proj1 2 (tuple 10, 20, 30, 40)
-eval proj2 2 (tuple 10, 20, 30, 40)
+check proj1 (pair 10 20)
+eval proj1 (pair 10 20)
+eval proj2 (pair 10 20)
+eval proj2 (pair 10 (pair 20 30))
+eval proj1  (pair 10 (pair 20 30))
+eval proj1 (proj2 (pair 10 (pair 20 30)))
+eval proj2 (proj2 (proj2 (pair 10 (pair 20 (pair 30 40)))))
 definition NZ : Type := sig x : Nat, 1 ≤ x
 variable t : NZ
 check proj1 t
diff --git a/tests/lean/sig4.lean.expected.out b/tests/lean/sig4.lean.expected.out
index 57be39ca5..ce98d9783 100644
--- a/tests/lean/sig4.lean.expected.out
+++ b/tests/lean/sig4.lean.expected.out
@@ -1,11 +1,11 @@
   Set: pp::colors
   Set: pp::unicode
-proj1 (tuple 10, 20) : ℕ
+proj1 (pair 10 20) : ℕ
 10
 20
-tuple 20, 30
+pair 20 30
+10
 20
-30
 40
   Defined: NZ
   Assumed: t
diff --git a/tests/lean/sig5.lean b/tests/lean/sig5.lean
index d417860e7..ab3de534c 100644
--- a/tests/lean/sig5.lean
+++ b/tests/lean/sig5.lean
@@ -2,8 +2,8 @@ variable vec : Nat → Type
 definition vec_with_len := sig len, vec len
 variable n : Nat
 variable v : vec n
-check tuple n, v
-check (show vec_with_len, from tuple n, v)
-check (let v2 : vec_with_len := tuple n, v
+check pair n v
+check (show vec_with_len, from pair n v)
+check (let v2 : vec_with_len := pair n v
        in v2)
-check (tuple vec_with_len : n, v)
+check (pair n v : vec_with_len)
diff --git a/tests/lean/sig5.lean.expected.out b/tests/lean/sig5.lean.expected.out
index caf59621c..48f140aeb 100644
--- a/tests/lean/sig5.lean.expected.out
+++ b/tests/lean/sig5.lean.expected.out
@@ -4,7 +4,7 @@
   Defined: vec_with_len
   Assumed: n
   Assumed: v
-tuple n, v : ℕ ⨯ vec n
-let H_show : vec_with_len := tuple (sig x : ℕ, vec x) : n, v in H_show : vec_with_len
-let v2 : vec_with_len := tuple (sig x : ℕ, vec x) : n, v in v2 : vec_with_len
-tuple vec_with_len : n, v : sig len : ℕ, vec len
+pair n v : ℕ ⨯ vec n
+let H_show : vec_with_len := pair n v : (sig x : ℕ, vec x) in H_show : vec_with_len
+let v2 : vec_with_len := pair n v : (sig x : ℕ, vec x) in v2 : vec_with_len
+pair n v : vec_with_len : sig len : ℕ, vec len
diff --git a/tests/lean/sig6.lean b/tests/lean/sig6.lean
index 3f6dc5712..620d7b1be 100644
--- a/tests/lean/sig6.lean
+++ b/tests/lean/sig6.lean
@@ -1,8 +1,8 @@
 variables A B : (Type U)
 variables t1 t2 : A ⨯ B
-axiom pair_Ax {A : (Type U)} {B : A → (Type U)} (p : sig x, B x) : (tuple (sig x, B x) : (proj1 p), (proj2 p)) = p
+axiom pair_Ax {A : (Type U)} {B : A → (Type U)} (p : sig x, B x) : (pair (proj1 p) (proj2 p) : sig x, B x) = p
 theorem spairext {A B : (Type U)} {p1 p2 : A ⨯ B} (H1 : proj1 p1 = proj1 p2) (H2 : proj2 p1 = proj2 p2) : p1 = p2
-:= calc p1  = tuple (proj1 p1), (proj2 p1)  :  symm (pair_Ax p1)
-        ... = tuple (proj1 p2), (proj2 p1)  :  { H1 }
-        ... = tuple (proj1 p2), (proj2 p2)  :  { H2 }
+:= calc p1  = (pair (proj1 p1) (proj2 p1))  :  symm (pair_Ax p1)
+        ... = (pair (proj1 p2) (proj2 p1))  :  { H1 }
+        ... = (pair (proj1 p2) (proj2 p2))  :  { H2 }
         ... = p2                            :  pair_Ax p2
\ No newline at end of file