From bc2d504cccd0cf488e11a5dca1bb749a6e7ccdaf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 30 Jan 2014 22:38:35 -0800
Subject: [PATCH] feat(builtin/kernel): add rewrite rules for if-then-else

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/kernel.lean      |   2 ++
 src/builtin/obj/kernel.olean | Bin 38337 -> 38400 bytes
 2 files changed, 2 insertions(+)

diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 11af8252c4..080da21722 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -677,6 +677,8 @@ theorem if_a_a {A : TypeU} (c : Bool) (a: A) : (if c then a else a) = a
      (λ H : ¬ c, calc (if c then a else a) = (if false then a else a) : { eqf_intro H }
                                     ...  = a                          : if_false a a)
 
+add_rewrite if_true if_false if_a_a
+
 theorem if_congr {A : TypeU} {b c : Bool} {x y u v : A} (H_bc : b = c)
                  (H_xu : ∀ (H_c : c), x = u) (H_yv : ∀ (H_nc : ¬ c), y = v) :
         (if b then x else y) = if c then u else v
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 4f90998b4c836178ec72570f21a945f7731297e1..98684cbb49d824d81a7e7b550b2f0beced71cff3 100644
GIT binary patch
delta 480
zcmX@OnyFz8(}sCX_K7Je@kK=pATX0DGcCTPs5F%UT`(;%rx;T-F+P!D^1P<kDaSy%
zrCEUl^KlT970f(=V4egq<-ww-Kuk|C^E8MV0%o28G26h*vp^QpM=<jokjZfm%)GGq
zZSxFP#-o$lI^&eCf>c8+xrSg~M=)<}X6u^D$arP)oNhm*+X(SH2<BY`^WJ8j9w|n~
zTa(p$=UO}hi9`JI7{PpkQ2i9dd<b^bGY}Kvm*<=R^y;!QKAfyId9USbkT}GQHy|d&
zsc%6{9<auDASNU{-h-H)8q7eF`Qc=RDMl=>fXvBylf@?IOzG482$F^v^$Em;81)&%
Ygc$V&#Dp02b+Y<YFUAj(i>CSm02td{KmY&$

delta 409
zcmZoz!*p;p(}sCXlkYaYPC3i~1k$WPg82xD$qHs3MKF(nnDSuJ;~=Idn0W%k3;{Dw
zf|zY!<|!bH=_8nV8p!0h2WFn#tkW`smGRKzqn&X|mq4l^mRv?KuOOILH@kLCWn{cK
z`F6LT(hY?8O$756f_ZzhcaIb!<MqjDy>l(@gTx_zd4OO(1Ti5tJ_0cxf*ti3#Dw_e
z$!6<5T~@|>lQSppwR`~*hnVpa#Dr*k1!D4mHNFNhA>r``#Prl)29nJ8CdW@PVthV%
o(v;=8??B=ZGv0%k5Hmi2m=H5Qf|w99K21)W>c#kW^2VwD0D$F6!vFvP