From 4c76f6abb93daccb32e4a047f807487ea0e2ad02 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Feb 2014 11:39:26 -0800 Subject: [PATCH] chore(builtin/num): remove leftover Signed-off-by: Leonardo de Moura --- src/builtin/num.lean | 2 -- src/builtin/obj/num.olean | Bin 32910 -> 37655 bytes 2 files changed, 2 deletions(-) diff --git a/src/builtin/num.lean b/src/builtin/num.lean index 98fab18ed..5cff6efad 100644 --- a/src/builtin/num.lean +++ b/src/builtin/num.lean @@ -557,8 +557,6 @@ add_rewrite mul_onel mul_oner theorem mul_comm (a b : num) : a * b = b * a := induction_on b (by simp) (by simp) -exit - theorem distributer (a b c : num) : a * (b + c) = a * b + a * c := induction_on a (by simp) (by simp) diff --git a/src/builtin/obj/num.olean b/src/builtin/obj/num.olean index d5749bc9d73bf878c2168533869684e86fa11b66..6f986a4aef140ed6b3e594d196ed3f4b9fe4482c 100644 GIT binary patch delta 3519 zcmZ`+&2Lpj6rbL{cW0)RSY9h%#Yly=TG2#EG%=Nercf%TC@cG6`=sCPgHm3j#e~*H z8xsr>ZVY}vq1ZGC2|<%uabaC`<3^Vl@E<^3xB;Y5&+nZ3?!0$}COthf=ggV&`McAT zA9!cxy=&8x71@53Q26N{IGPU4Un%Gq-`qfu8 zQEwO4CzyT3v9AW{_tpeI9;sNXAksU;46&vQq&;|Is501e*w*H5fYv7R_7ht{)+v8ccOn0>T?fOGLVbr6;cZ3vTIW25;En(Mko$uGvwN(+y;x3 z#!Y%6x2apJv7RKN%0SRn=3?yT^O1Y1EMko$Pg06gvmi02_ZWB9WT3DJay?#q=lh^z zS)T)1L@YyQ5NEL~VZI-8Q-*^Nz!!;S5e~c5s|J?n`J(;zES zi91kpl`t!i-4g{M(;Z<6nd%Me`q2kNdn|JOqd{~wZQ4^B$`E)&P-qE}(l+=c|l^HCa(SS1Ny>U=I@RU&4Ejh?~!86cG|DvZRI ziUH`}hZe)x3PrMhl`Y{Y7#{A2Q6vu7lANv|>kC`*AZIuZsmA?k?v|anhc6NYP2skb zEpxX?0U3@hTEJjKz80K|@G!?V0lBzd7@E1~Lc1HW5}-84L-lP{?o!V_$=;cn$h%M| z9}6UhH{!`Kd0mX0^7q$P!4C<6Yn=Dd<#N_UesadxSvjP+hHQy3iyP&wPz$GcBlHae zq5&_QxG-cWxe+ugaj0#Kpf)o$91IR_qo-72yWAi!7&TZ3v9FQE5MuW^_Vo~ASJ!bc ze2C{5up9zzv}xLTlYn6DOHQ4`#KS1W-{|7_6U)Md@QG#jg2xlfHiu8FglG4j9$#0( zq7bnPi_Ve|(4z6RO?VApq-)c$bnrd?0_$UH6g;s#;E)R2=hEL6 zWy$vEaOa?HgH}J0IELD`$f($3%l+7tso_kzsR@+?jF7;bFLc+s7i}-CZ5O-1)7=>h zq_;3+e#O}?YLj()@>pNXKwz6+1GqR5u5a6H^U z(>U*j+NSeoxO2FtH`{sea3(_!rrI}fT>hEiMu4U8AEEukhI0(9kbRTcr-|z0%o5@6 qqPbm6tk)cTeQ49O&2boM>F()O-k~wPI+gkm