Leonardo de Moura 70b27fb2d3 feat(library/init/meta/interactive): unfold is now based on the simp framework ... See issue #1694. There is an orthogonal issue. `simp` (and consequently `unfold`) cannot be used to reduce projections (e.g., `has_add.add`). This issue has been previously raised by @Armael, but it was not addressed yet.		2017-07-02 11:30:48 -07:00
..
basic.lean	feat(init/data/int): int lemmas, more bitwise theorems	2017-06-27 18:55:52 -07:00
bitwise.lean	feat(library/init/meta/interactive): unfold is now based on the simp framework	2017-07-02 11:30:48 -07:00
comp_lemmas.lean	feat(library): add mk_int_val_ne_proof	2016-12-24 15:22:31 -08:00
default.lean	feat(init/data/int): int lemmas, more bitwise theorems	2017-06-27 18:55:52 -07:00
lemmas.lean	feat(init/data/int): int lemmas, more bitwise theorems	2017-06-27 18:55:52 -07:00
order.lean	feat(init/data/int): int lemmas, more bitwise theorems	2017-06-27 18:55:52 -07:00