Leonardo de Moura dc5ca99afa 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`.		2016-01-24 13:37:15 -08:00
..
basic.lean	fix(library/data/real/basic): unnecessary level of indirection	2016-01-24 13:37:15 -08:00
complete.lean	feat(library/unifier): remove "eager delta hack", use is_def_eq when delta-constraint does not have metavariables anymore	2016-01-03 12:39:32 -08:00
default.lean	refactor(library): remove algebra namespace	2015-12-05 23:50:01 -08:00
division.lean	refactor(*): normalize metaclass names	2015-12-28 10:39:15 -08:00
order.lean	refactor(*): normalize metaclass names	2015-12-28 10:39:15 -08:00
real.md	feat(library/data/{int,rat,real}/bigops): add bigops for int, rat, real	2015-08-08 17:20:23 -04:00