michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/data/real/basic): unnecessary level of indirection

Browse source 
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`.
This commit is contained in:
Leonardo de Moura 2016-01-24 13:37:15 -08:00
parent b2554dcb8f
commit dc5ca99afa
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/data/real/basic.lean
View file

@ -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,