Skip to content

[Merged by Bors] - fix: add missing no_index around OfNat.ofNat #8317

Closed
eric-wieser wants to merge 5 commits intomasterfrom
eric-wieser/noindex-fixes
Closed

[Merged by Bors] - fix: add missing no_index around OfNat.ofNat #8317
eric-wieser wants to merge 5 commits intomasterfrom
eric-wieser/noindex-fixes

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented Nov 10, 2023 •
edited by github-actions bot
Loading

eric-wieser and others added 2 commits November 10, 2023 12:42
@eric-wieser @timotree3
chore: add missing no_index around OfNat.ofNat library notes
2b0050f 
Co-authored-by: timotree3 <timorcb@gmail.com>
@eric-wieser @timotree3
fix: add missing no_index around OfNat.ofNat
dfb9ef9 
Co-authored-by: timotree3 <timorcb@gmail.com>
@eric-wieser eric-wieser added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Nov 10, 2023
@eric-wieser eric-wieser mentioned this pull request Nov 10, 2023
Closed
1 task
@eric-wieser
Copy link
Copy Markdown
Member Author

eric-wieser commented Nov 10, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Nov 10, 2023

Here are the benchmark results for commit dfb9ef9.
There were no significant changes against commit 7a1bf93.

timotree3
timotree3 reviewed Nov 10, 2023
View reviewed changes
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 10, 2023
@ghost
Copy link
Copy Markdown

ghost commented Nov 10, 2023

This PR/issue depends on:

@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 Nov 12, 2023
@timotree3 timotree3 mentioned this pull request Nov 12, 2023
Open
1 task
jcommelin
jcommelin approved these changes Dec 4, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Dec 4, 2023
mathlib-bors bot pushed a commit that referenced this pull request Dec 4, 2023
@eric-wieser @timotree3
fix: add missing no_index around OfNat.ofNat (#8317)
070be71 
Co-authored-by: timotree3 <timorcb@gmail.com>



Co-authored-by: timotree3 <timorcb@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 4, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title fix: add missing no_index around OfNat.ofNat [Merged by Bors] - fix: add missing no_index around OfNat.ofNat Dec 4, 2023
@mathlib-bors mathlib-bors bot closed this Dec 4, 2023
@mathlib-bors mathlib-bors bot deleted the eric-wieser/noindex-fixes branch December 4, 2023 13:54
awueth pushed a commit that referenced this pull request Dec 19, 2023
@eric-wieser @timotree3 @awueth
fix: add missing no_index around OfNat.ofNat (#8317)
6513764 
Co-authored-by: timotree3 <timorcb@gmail.com>



Co-authored-by: timotree3 <timorcb@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin approved these changes

+1 more reviewer

@timotree3 timotree3 timotree3 approved these changes

Reviewers whose approvals may not affect merge requirements

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.

4 participants

@eric-wieser @leanprover-bot @jcommelin @timotree3