Skip to content

[Merged by Bors] - chore: remove unused lemmas about bit0/1#14672

Closed
Ruben-VandeVelde wants to merge 1 commit intomasterfrom
deprecated-bits
Closed

[Merged by Bors] - chore: remove unused lemmas about bit0/1#14672
Ruben-VandeVelde wants to merge 1 commit intomasterfrom
deprecated-bits

Conversation

@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde commented Jul 12, 2024

Open in Gitpod

@Ruben-VandeVelde Ruben-VandeVelde added the tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip label Jul 12, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 12, 2024

PR summary dc87bafa04

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

- ofNat_bit0
- ofNat_bit1
- zpow_bit0
- zpow_bit0'
- zpow_bit1
- zpow_bit1'

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

grunweg
grunweg reviewed Jul 12, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

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

Also looks good to me, thanks! I'm not sure what the best strategy for landing #14644 is, but landing such removal-only pieces does not strike me as harmful.
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 12, 2024

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 12, 2024
jcommelin
jcommelin reviewed Jul 12, 2024
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

mathlib-bors bot pushed a commit that referenced this pull request Jul 12, 2024
@Ruben-VandeVelde
chore: remove unused lemmas about bit0/1 (#14672)
e0d8b5b
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Jul 12, 2024

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 12, 2024

✌️ Ruben-VandeVelde can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 12, 2024
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 12, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: remove unused lemmas about bit0/1 [Merged by Bors] - chore: remove unused lemmas about bit0/1 Jul 12, 2024
@mathlib-bors mathlib-bors bot closed this Jul 12, 2024
@mathlib-bors mathlib-bors bot deleted the deprecated-bits branch July 12, 2024 12:01
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@grunweg grunweg grunweg left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@Ruben-VandeVelde @jcommelin @grunweg