From 2753a0ffc005954ab4b27c369770e27ec01535d4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Jan 2014 20:56:35 -0800 Subject: [PATCH] fix(builtin/kernel): add ascii notation for transitivity Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 3 ++- src/builtin/obj/kernel.olean | Bin 25014 -> 25041 bytes 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 1edc637e9..561e371de 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -156,7 +156,8 @@ theorem symm {A : TypeU} {a b : A} (H : a = b) : b = a theorem trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c := subst H1 H2 -infixl 100 ⋈ : trans +infixl 100 >< : trans +infixl 100 ⋈ : trans theorem ne_symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a := assume H1 : b = a, H (symm H1) diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index b11d31aedb1cdcf6d733e4ba22166aad8e66ab3f..22631630eb7ef9e1adcfae01f38555e2460b09d0 100644 GIT binary patch delta 2582 zcmZvdYgANK6vt;@88E%HB+$znW|#rRabSdj;Wa!29TX857)1oZD9Z=%N}d_3Lk0aGczBc-F*&mzVzj+-`(fG|9hXg=kD3t z0Vg}4{lg){?Wr0`qtR5;qUqA)*Va|lyXyd&0&T55v1eUWwH{3%;@VRjfP!1uLxGG1`iKQ^WG?6ocz_@?`;DHWgz1I^9Qg4@kT-$k^mNv5T@_6odUw!>-+i)n$i zxGTmAZ{g(_JFG)PY#VIAld#c4tBHLeVAY^kq?T^ zLp)c;)Pws+tW2ILpQSJt zpTmyiWYyzI@-gM22wx)P9+&ag6djyl-E^T}>UjC8&|SmXsjn;7MSx9oo_GU2(@gL? zOZ)@#(w3TUla7BHcL=%eE+PLkXs&w{M6uhd!^dg0a1UqNuc%*rQF<2K!nNs3^=w*m zlWxl7CN!;kO`f1FqZ=NfHPfMZQkaP)Hi?;7>W^<{8dSUe>iP)JWrl#(-JO{MdRfT5 zRrF}5pH3P?xQC&yyJFNxfPuI=yTZW6BfFInjYob#rErGB=nT?84Ia%g$VQd>+1aVy zz&km9I5EeeL@*t56*E#Y;@+HOn4+pS;`-4>-(FLbD)#7RVzaw*bTs(H(H{|g-CCIr zDaEaE#KJphakzYFB=Uii%(kq!-cb$l*yCu153ngW!N;a5STYnch0T2`cMm`mHjb-9 zue`ppqg0vJ$;#%q=%f_ zW>+x2SKtTv=q{L!#=<`HGLrE#O~InVdEmm%!k5riWDM&yeV$Btc{0_uaZfwWEsBE* z+*ULJpB5SW_o`>1&Z(#-NzN#kj#bY2c;4ApY(DFWoum%s;y|!qRPh$5QFVjye6bVL zO8T@*s8$!#*5izlW_3W4%G;HKPFLTF8%gy)C$3RX91F|vu9j)KUNd delta 2525 zcmYL~dr;I>6vy}c++7ftQ6BQ+z3lQ{c`P6-AS`cM6oh4AO_BAHiQ^1v>SPK!Drr6- z98Z%IVW~9sq9k|JOf&Pek7ah*z1sZ_IQQT3^?H(-kK58^Nlt+#0LV0fF*o8cX-kh9<>z9KKpy-Q&( z{)>={?-6qGeL@4P`&%JsX7~@`RxAkeM|+?R`mrN$ZstRha<2hG?)8X}dp#!PUV{q3 zF6K3aIYH&{0M`eZy;c8`L_={<;fbIec!I-%lXUESJUk3@gRKDA9K0q|OKR2;JOp|Y z1~QM~gslv{2y+>Zz^stjpuue+^D{?Lm|OS=^d)4Q20uc!Y49f;Viu$Enb0~IiCv+c z69XyCErJ9F6Y^bz5b|Aw67pSy5!#qrxI!?%P>*e4<%;poVbP%393BfY#)U6TG?1A0 zFcKy(aU>ysEKv$cyj?VY6`l|A=&8?#2rSdvjR~aV)ro|>I*E`UG8qr*3t$XB(bpT( zD9laA3QQ;D{u%D&5uu>GnGVBANW})DJvmPZ^92?V@|r@0Bx?-4M@UuSWxXHjEyKZz z>d1UuG3j{660C|G2SwN#nWrlg;qiDj(g`+9ikeV3k;42im4xh?K@}lCj9npUk7B)S z6ozJ6J<1vvuwNB;AZonMLCl-hxP79NK%Och^#WaPXH2jJbMb|^Eiey<$8Uj!xII4F zubMO}cG)~4S+hnw7oX$3nAP(3MQAiV4@(riKX#f7um}&CQeY|eo2KZRn2x>2W^|4@ z4J$DrVUPT>2(J;i*8MOc2VeuHC$+(=ik}~zN%HkuMhaCnEl>Bb9v>%JVH0L2x5H~p zcOlsb?VHV3cpdZ1-Oz!0os7d$O5rU=Gg7Ru1Gl9V!aMBuqm)|RyJX0p&3m}q5`j&r z*W`~x@MD3ya7mg0cH$^YAavvIv@+c%BDtFt$Bz9;-Y0^e3fzwY=?3Uw#e317UaLDG zk_TC_cZL_9Pw$t%6p14OkK&b#1o(^@9L9KyO?O-*Pq>#`v>=}pk#7WkiyfH;IL0c! z#?zU_^7kUyEAR(2XQjY*I5Vr=c#6Wn-q>kE{u!Mi3}?}^=$G99KVnn%B;9!mbMXcI zH9K4J2pV@x?i1lFgxupQ-XCXxU)XLgV{%S~?l+afX2K+xT6@YGP1$V zP1xY(CWFFc2p#!@Fo0DBHkppkJ4$RQGqL1>y9%NdyHmT6x-XTQz$X=y41LiW9i2i-#Sohr-oSF3Gk|6x&}dO* zvmF185jKB3X`29P7+BT@UAVI>!^c7@vH?4jTHLqG_5j3S*M!AdD*Cp>YLoxd7SB=7?l|_Wa`1(VC4K$u@1~EQ+WHxwIB* z9I-GPn;na^^SJb;!xX6=V*6f1%Aq)AmDryv1yve$Vlx)j?0`nRRx?NY5(}fPRylAV zD_ntVYTJ~l=;y4`w(zXW$q(A795fVweJ WZNG3ErfmQ?g5A?E!a;1EQSu*G&cx~f