Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - chore: move Int.coe_nat_strictMono #13197

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore: move Int.coe_nat_strictMono #13197

wants to merge 1 commit into from

Conversation

Ruben-VandeVelde
Copy link
Collaborator

Open in Gitpod

@Ruben-VandeVelde Ruben-VandeVelde added awaiting-review The author would like community review of the PR awaiting-CI labels May 25, 2024
YaelDillies
YaelDillies reviewed May 25, 2024
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Nicely spotted. Move you mind taking the opportunity to rename it to Int.natCast_strictMono (with deprecation?

@YaelDillies
Copy link
Collaborator

Actually, there's more than that lemma to rename, so I'll fix everything later.

maintainer merge

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@sgouezel
Copy link
Contributor

bors r+

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label May 25, 2024
mathlib-bors bot pushed a commit that referenced this pull request May 25, 2024
@Ruben-VandeVelde
chore: move Int.coe_nat_strictMono (#13197)
dacd3b1
@github-actions github-actions bot removed the awaiting-review The author would like community review of the PR label May 25, 2024
@YaelDillies YaelDillies mentioned this pull request May 25, 2024
Closed
1 task
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 25, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: move Int.coe_nat_strictMono [Merged by Bors] - chore: move Int.coe_nat_strictMono May 25, 2024
@mathlib-bors mathlib-bors bot closed this May 25, 2024
@mathlib-bors mathlib-bors bot deleted the Int.coe_nat_strictMono branch May 25, 2024 12:38
callesonne pushed a commit that referenced this pull request Jun 4, 2024
@Ruben-VandeVelde @callesonne
chore: move Int.coe_nat_strictMono (#13197)
78e89ef
js2357 pushed a commit that referenced this pull request Jun 18, 2024
@Ruben-VandeVelde @js2357
chore: move Int.coe_nat_strictMono (#13197)
bf2269e
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@YaelDillies YaelDillies YaelDillies left review comments

Assignees
No one assigned
Labels
maintainer-merge 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.

None yet
3 participants
@Ruben-VandeVelde @YaelDillies @sgouezel