From 78942a068952d023ae68d232bb25d30b80b44520 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Mon, 3 Aug 2015 16:38:42 -0400 Subject: [PATCH] fix(library/data/real): fix num -> rat -> real coercion chain --- library/data/real/basic.lean | 2 ++ library/data/real/complete.lean | 4 ++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index 813793e1e..f438912ec 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -1096,6 +1096,8 @@ protected definition comm_ring [reducible] : algebra.comm_ring ℝ := apply mul_comm end +open rat -- no coercions before + definition of_rat [coercion] (a : ℚ) : ℝ := quot.mk (s.r_const a) theorem of_rat_add (a b : ℚ) : of_rat a + of_rat b = of_rat (a + b) := diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index 5f7813f26..b503bef61 100644 --- a/library/data/real/complete.lean +++ b/library/data/real/complete.lean @@ -452,7 +452,7 @@ theorem ex_smallest_of_bdd {P : ℤ → Prop} (Hbdd : ∃ b : ℤ, ∀ z : ℤ, have Heltb : elt > b, begin apply int.lt_of_not_ge, intro Hge, - apply false.elim ((Hb _ Hge) Helt) + apply (Hb _ Hge) Helt end, have H' : P (b + of_nat (nat_abs (elt - b))), begin rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !int.sub_pos_iff_lt Heltb)), @@ -489,7 +489,7 @@ theorem ex_largest_of_bdd {P : ℤ → Prop} (Hbdd : ∃ b : ℤ, ∀ z : ℤ, z have Heltb : elt < b, begin apply int.lt_of_not_ge, intro Hge, - apply false.elim ((Hb _ Hge) Helt) + apply (Hb _ Hge) Helt end, have H' : P (b - of_nat (nat_abs (b - elt))), begin rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !int.sub_pos_iff_lt Heltb)),