From 840f0ea05d5ff773040a2d7e38dc66264d65591c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Oct 2015 15:13:16 -0700 Subject: [PATCH] fix(library/theories/analysis/real_limit): minor --- library/theories/analysis/real_limit.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean index c11c7f6a5..5cd885b57 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -21,7 +21,7 @@ These could be avoided in a constructive theory of analysis, but here we will no follow that route. -/ import .metric_space data.real.complete -open real eq.ops classical +open real classical algebra noncomputable theory namespace real @@ -32,7 +32,7 @@ protected definition to_metric_space [instance] : metric_space ℝ := ⦃ metric_space, dist := λ x y, abs (x - y), dist_self := λ x, abstract by rewrite [sub_self, abs_zero] end, - eq_of_dist_eq_zero := @eq_of_abs_sub_eq_zero, + eq_of_dist_eq_zero := λ x y, algebra.eq_of_abs_sub_eq_zero, dist_comm := abs_sub, dist_triangle := abs_sub_le ⦄