From 15c9ec12cf2980756c25088c5601dd0c489bc0b1 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sun, 14 Feb 2016 10:16:13 -0500 Subject: [PATCH] fix(library/data/real/division): make temporary has_div only a local instance --- library/data/real/division.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/library/data/real/division.lean b/library/data/real/division.lean index 87f9af41fe..1d995d52c9 100644 --- a/library/data/real/division.lean +++ b/library/data/real/division.lean @@ -593,9 +593,11 @@ noncomputable definition real_has_inv [instance] [reducible] [priority real.prio noncomputable protected definition div (x y : ℝ) : ℝ := x * y⁻¹ -noncomputable definition real_has_div [instance] [reducible] [priority real.prio] : has_div real := +noncomputable definition real_has_div : has_div real := has_div.mk real.div +local attribute real_has_div [instance] [reducible] [priority real.prio] + protected theorem le_total (x y : ℝ) : x ≤ y ∨ y ≤ x := quot.induction_on₂ x y (λ s t, rat_seq.r_le_total s t)