From dc5ca99afae406f710dd671f7fce0afced8d9796 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 24 Jan 2016 13:37:15 -0800 Subject: [PATCH] fix(library/data/real/basic): unnecessary level of indirection At real.comm_ring, `add` is `@add real real_has_add`. This is bad for any tactic (e.g., blast) that only unfolds reducible definitions. `add` is not reducible. So, the tactic will not be able to establish that `@add real real_has_add` is definitionally equal to `real.add`. --- library/data/real/basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index 22cf83401c..5e2b5b1146 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -1148,15 +1148,15 @@ protected theorem zero_ne_one : ¬ (0 : ℝ) = 1 := protected definition comm_ring [reducible] : comm_ring ℝ := begin fapply comm_ring.mk, - exact add, + exact real.add, exact real.add_assoc, exact of_num 0, exact real.zero_add, exact real.add_zero, - exact neg, + exact real.neg, exact real.neg_cancel, exact real.add_comm, - exact mul, + exact real.mul, exact real.mul_assoc, apply of_num 1, apply real.one_mul,