-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Faster #391
Faster #391
Conversation
Can you PR |
How do I do that? |
I just pushed a `squeeze-simp` branch to community, that just has
squeeze_simp, without using it to speed up the library.
…On Sat, Oct 6, 2018 at 11:41 PM Kenny Lau ***@***.***> wrote:
How do I do that?
—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
<#391 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AAdLBGGFYDeJkSoUCdTpbXYdZw3Oy9bMks5uiLMcgaJpZM4XKeZX>
.
|
(Kenny --- to do this I checked out the master branch, ran `git merge
--squash faster`, then threw out all the modified files except the ones in
the `tactic` directory, created a new branch, and committed.)
…On Sun, Oct 7, 2018 at 12:01 AM Scott Morrison ***@***.***> wrote:
I just pushed a `squeeze-simp` branch to community, that just has
squeeze_simp, without using it to speed up the library.
On Sat, Oct 6, 2018 at 11:41 PM Kenny Lau ***@***.***>
wrote:
> How do I do that?
>
> —
> You are receiving this because you are subscribed to this thread.
> Reply to this email directly, view it on GitHub
> <#391 (comment)>,
> or mute the thread
> <https://github.com/notifications/unsubscribe-auth/AAdLBGGFYDeJkSoUCdTpbXYdZw3Oy9bMks5uiLMcgaJpZM4XKeZX>
> .
>
|
f3153d4
to
bbf9c08
Compare
#396 has been merged. |
algebra/group_power.lean
Outdated
@@ -51,37 +51,39 @@ attribute [to_additive succ_smul] pow_succ | |||
attribute [to_additive add_monoid.one_smul] pow_one | |||
|
|||
theorem pow_mul_comm' (a : α) (n : ℕ) : a^n * a = a * a^n := | |||
by induction n with n ih; simp [*, pow_succ, mul_assoc] | |||
nat.rec_on n (by rw [pow_zero, one_mul, mul_one]) $ λ n ih, | |||
by rw [pow_succ, mul_assoc, ih] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Don't use nat.rec_on
, break out the original proof onto multiple lines or use the tac; [tac1, tac2]
format
@@ -13,6 +13,53 @@ import logic.function order.boolean_algebra | |||
|
|||
open list subtype nat lattice | |||
|
|||
run_cmd mk_simp_attr `multiset |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you do this without adding a new simp set?
9842bcd
to
18b0e47
Compare
2083b65
to
db5de9c
Compare
@digama0 As I understand it, some of this is merged and some is WIP? Maybe we could close this PR and Kenny can open a new one when there's more to add? |
I think it's all merged except for |
@kckennylau, would you mind if this was closed now? |
Ok. |
TO CONTRIBUTORS:
Make sure you have:
For reviewers: code review check list