From 534838a36c6c6773aff5677e7d1e086835082db5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2014 18:30:45 -0800 Subject: [PATCH] chore(build): update automatically generated files Signed-off-by: Leonardo de Moura --- src/builtin/obj/if_then_else.olean | Bin 3089 -> 5053 bytes src/library/CMakeLists.txt | 2 +- src/library/if_then_else_decls.cpp | 3 +++ src/library/if_then_else_decls.h | 9 +++++++++ 4 files changed, 13 insertions(+), 1 deletion(-) diff --git a/src/builtin/obj/if_then_else.olean b/src/builtin/obj/if_then_else.olean index c085ab55abe9aaec902d3ff4f4a9972d6f5753fe..202e92997eff569f26b1bba1b3eaeb3796a3fac4 100644 GIT binary patch literal 5053 zcmbtY&2Jk;6rY{7*L>vw7801Rpw@P(VpSz@;7dvh6qmGVDMd(p$XYvVy24pI_Bu-b zjGib54shU@Q*Ura;y<7%aDoG85Vr#J`@P-FX1Y-$v4_!b-h1=joA;Z2JN9@Kg~>1; zMJju|cyltIrt0%(nnWX&&DO(I_2=;@jT7a^X{0V}PLu{PkLRtA(=d(431+^Ihf1f{ zqeSUwG>cT#2s>Jg!yU6~*h{DLNCkRTX?<;X5`Cb|Bvc-j2f9z-HMNemjB_K?Eod^e z=3)p`1%pq7eDENc=Vf7rA>tzr9*r1ye8j+0X=20@6&wm73n4GW@begt7_sN2*SVFj z7ZxK7%$ClL$0OMh9h3)gd}Hb}lg9uxVI8ne_&8vtrS%{*TT)fM1A(eHF;-C;-|nCR zq0|M4WvVnaFrBFYkOsbpu_co-1`z{Q@(n*~CI=fHjFZo%#Vt!M>wz9%kupGX3j)1M zNh8p6vR4W8HbFJe-Clp7BzvyH(8kb$Zf9;HbbI2lZ8!PAfthjI?d@*UEE%X1S|{UF z4oP6`AGG#1))`x=Gti&H(816yXi(D{gp@U^fKOr&ZdhaC<|#-8J`EVq_8CA~_AFqF z(&qr%go}VngwF$>COiRnc1i2;v=@!yO-z+qruYTIrjPf+JhBgg7~OqX%`%|u!xSpY zomLM@yleud(=eGy1s}3?xPYZB6PPc9d&Y8JiHxZ+)v==AobPQ>hiBFF_flNb+ zz~dCa$TvM@w!4`f37V`yE-#&3S76enPZmxcD}9=}FB$8}s)@$g(;7>#fpiMh!t_%d zUGv)GS-lVU3ow%OfiAk{5HiqKnTCnAT#e<16=MjgEWCAGa|qWlOfh^&wXGr#0bP6q z^~Yp#cm$J+Fmah=hnEikt3^GVM2qy>MWr+{_VH+>X$LvbQ|vIdRmK?Cr1{6>3A485 z$&-CUno-brqmZtk6?RYlHj5O$%tn_8T8|EN| z0IHF_K(^`1%i4vK$FE^o=bTeUWF|GsdZ{_z0Be4e%Sji_zhn~jZ51C72F`h*Bl(=T zO{4ClD5mu6X!zDq*03B(B2HqQ)@bwzJaO*JoESo>5T|yF2N#I5#=tj}7x?DYFsJPZ zzTx)V1-NH8jL2x1r?=j~uAeE9@Y6A#wVsKe3Tnt$q9%j2m zm&IG~As3KEz@u5DqvNqCrf|o=Upa)`V%awi!g0DlqZx#plkacym+%!M&It)8lb*Sg zZ^W~78u#bsPG7h&pMwKjou$_rqJ~B-^<>e^EiZe2@^@BR4k>DpxIzipG`NWh{1)!4 zOtK;NP*LBfmsQN=*2Q!Lz6q(&{}$j6v^@_f4d5L>>D()T47=9^q?=-L5K2dLlcPqG z1N;#~pJ`^Hbaw!mDs+oB^@VoPfdQQaKovp{kOirUJ?4Rht`!&EhS9$5G+h4^gw)(| zHKm!LsxdU|DT2ff3x&3G}X8G$|xFa)?(91}2 zzzGX)1+7@5KN0^gr$|id8}zXO)N0Qqnf~l?T7Z!x4fL~X4&gqAyRL@py62Ye0@znD z$lo%gO26w^w zWxx0#<$mvJq0kiS!DCT}u;4^i($adiLSc$O1EkkpgsJq}OMqg)8?C&jJPwT|4dn_3 zNlxOjMoiv@kPP!e;kQwFokqov(f_EE$HP=8R%uC?mG6|Kg6+tEGw%UPNv;A)N!|yP zl3W9nlCbmequ|jY_byTMADM+OB@d@hM|44ymj^$SJn!-(RQwmsdpp@UkH75x12m&c Ag8%>k delta 31 mcmdn1K2c&qI-||TjOpA${soB)OqnIA42-UMDQ=lLsSE(5O$mzt diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 2b7047eca..cf1b7486a 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,6 +1,6 @@ add_library(library kernel_bindings.cpp deep_copy.cpp context_to_lambda.cpp placeholder.cpp expr_lt.cpp substitution.cpp fo_unify.cpp bin_op.cpp equality.cpp io_state_stream.cpp printer.cpp - hop_match.cpp ite.cpp) + hop_match.cpp ite.cpp heq_decls.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/if_then_else_decls.cpp b/src/library/if_then_else_decls.cpp index 57c5b08dc..91dfc556a 100644 --- a/src/library/if_then_else_decls.cpp +++ b/src/library/if_then_else_decls.cpp @@ -12,4 +12,7 @@ MK_CONSTANT(if_a_a_fn, name("if_a_a")); MK_CONSTANT(if_congr_fn, name("if_congr")); MK_CONSTANT(if_imp_then_fn, name("if_imp_then")); MK_CONSTANT(if_imp_else_fn, name("if_imp_else")); +MK_CONSTANT(app_if_distribute_fn, name("app_if_distribute")); +MK_CONSTANT(eq_if_distributer_fn, name("eq_if_distributer")); +MK_CONSTANT(eq_if_distributel_fn, name("eq_if_distributel")); } diff --git a/src/library/if_then_else_decls.h b/src/library/if_then_else_decls.h index cc511ccca..af787b429 100644 --- a/src/library/if_then_else_decls.h +++ b/src/library/if_then_else_decls.h @@ -23,4 +23,13 @@ inline expr mk_if_imp_then_th(expr const & e1, expr const & e2, expr const & e3, expr mk_if_imp_else_fn(); bool is_if_imp_else_fn(expr const & e); inline expr mk_if_imp_else_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_if_imp_else_fn(), e1, e2, e3, e4, e5}); } +expr mk_app_if_distribute_fn(); +bool is_app_if_distribute_fn(expr const & e); +inline expr mk_app_if_distribute_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_app_if_distribute_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_eq_if_distributer_fn(); +bool is_eq_if_distributer_fn(expr const & e); +inline expr mk_eq_if_distributer_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_eq_if_distributer_fn(), e1, e2, e3, e4, e5}); } +expr mk_eq_if_distributel_fn(); +bool is_eq_if_distributel_fn(expr const & e); +inline expr mk_eq_if_distributel_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_eq_if_distributel_fn(), e1, e2, e3, e4, e5}); } }