Skip to content

[Merged by Bors] - chore(Logic/Function/Basic): @[simp] lemmas#6303

Closed
kim-em wants to merge 1 commit intomasterfrom
of_comp_iff_simp
Closed

[Merged by Bors] - chore(Logic/Function/Basic): @[simp] lemmas#6303
kim-em wants to merge 1 commit intomasterfrom
of_comp_iff_simp

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Aug 2, 2023 •
edited
Loading

@kim-em kim-em added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Aug 2, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 2, 2023
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Aug 2, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 2, 2023
@ghost
Copy link
Copy Markdown

ghost commented Aug 2, 2023

This PR/issue depends on:

@kim-em kim-em force-pushed the of_comp_iff_simp branch 2 times, most recently from a0a7aee to 66ee3b6 Compare August 3, 2023 03:40
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Aug 3, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Aug 3, 2023

Here are the benchmark results for commit 66ee3b6.Found no runs to compare against.

@kim-em kim-em force-pushed the of_comp_iff_simp branch from 66ee3b6 to f6a97da Compare August 6, 2023 00:04
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Aug 6, 2023

!bench

@kim-em kim-em added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 6, 2023
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Aug 6, 2023

Here are the benchmark results for commit f6a97da.
There were no significant changes against commit 944ee07.

@kim-em kim-em added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Aug 6, 2023
@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Aug 8, 2023

I looked at the benchmark and it seems (to me) to be mostly noise, so I think it's fine to merge this.

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Aug 8, 2023
bors bot pushed a commit that referenced this pull request Aug 8, 2023
@kim-em
chore(Logic/Function/Basic): @[simp] lemmas (#6303)
e176cb0 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Aug 8, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title chore(Logic/Function/Basic): @[simp] lemmas [Merged by Bors] - chore(Logic/Function/Basic): @[simp] lemmas Aug 8, 2023
@bors bors bot closed this Aug 8, 2023
@bors bors bot deleted the of_comp_iff_simp branch August 8, 2023 23:08
kim-em added a commit that referenced this pull request Aug 14, 2023
@kim-em
chore(Logic/Function/Basic): @[simp] lemmas (#6303)
bc28dfd 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@kim-em @leanprover-bot @j-loreaux