Skip to content

[Merged by Bors] - style(DedekindDomain/AdicValuation): fix some snake_case to lowerCamelCase#14533

Closed
faenuccio wants to merge 6 commits intomasterfrom
fae_PR_lowerCamelCase_adicCompletion
Closed

[Merged by Bors] - style(DedekindDomain/AdicValuation): fix some snake_case to lowerCamelCase#14533
faenuccio wants to merge 6 commits intomasterfrom
fae_PR_lowerCamelCase_adicCompletion

Conversation

@faenuccio
Copy link
Copy Markdown
Contributor

@faenuccio faenuccio commented Jul 8, 2024

In some theorem names, int_valuation was still used instead of intValuation, and this PR fixes this.

@faenuccio
style(DedekindDomain/AdicValuation): fix some snake_case to lowerCame…
8d8fbd1 
…lCase

In some theorem names, `int_valuation`  was still used instead of `intValuation`, and this PR fixes this.
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 8, 2024 •
edited
Loading

PR summary 9806cf9290

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ adicCompletion.algebra'
+ adicCompletion.instCoe
+ adicCompletion.instIsScalarTower'
+ intValuation.le_max_iff_min_le
+ intValuation.map_add_le_max'
+ intValuation.map_mul'
+ intValuation.map_one'
+ intValuation.map_zero'
+ intValuation_exists_uniformizer
+ intValuation_le_one
+ intValuation_le_pow_iff_dvd
+ intValuation_lt_one_iff_dvd
+ intValuation_ne_zero
+ intValuation_ne_zero'
+ intValuation_zero_le
- AdicCompletion.algebra'
- AdicCompletion.instCoe
- AdicCompletion.instIsScalarTower'

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

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

@faenuccio faenuccio added awaiting-review easy < 20s of review time. See the lifecycle page for guidelines. labels Jul 8, 2024
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Jul 8, 2024

Thanks for pursuing this clean-up? Would you also like to rename int_valuation_exists_uniformizer and int_valuation_le_pow_iff_dvd?
Can you also add deprecation aliasses for the renamed theorems? (There is a script somewhere to generate these automatically, though I'm not sure what the current status is. @adomani might know, or you can ask on zulip.)

@grunweg grunweg added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jul 8, 2024
@faenuccio
Copy link
Copy Markdown
Contributor Author

faenuccio commented Jul 9, 2024

Thanks for pursuing this clean-up? Would you also like to rename int_valuation_exists_uniformizer and int_valuation_le_pow_iff_dvd? Can you also add deprecation aliasses for the renamed theorems? (There is a script somewhere to generate these automatically, though I'm not sure what the current status is. @adomani might know, or you can ask on zulip.)

Thanks, done! I will check this point about deprecation aliases.

@faenuccio
Copy link
Copy Markdown
Contributor Author

faenuccio commented Jul 9, 2024

OK done, I have discussed with @adomani (thanks!!!) and have added the deprecation aliases using the deprecate to tool. I had to manually remove the namespace from the aliases lest they would not work (but now they do).

@adomani
Copy link
Copy Markdown
Contributor

adomani commented Jul 9, 2024

Ah, thanks for the report on the namespace! I will try to take a look, but I'm not sure when I'll have the time!

@faenuccio faenuccio added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jul 9, 2024
@mariainesdff
Copy link
Copy Markdown
Contributor

mariainesdff commented Jul 9, 2024

Thanks!

@mariainesdff
Copy link
Copy Markdown
Contributor

mariainesdff commented Jul 9, 2024

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 9, 2024

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 9, 2024
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Jul 9, 2024

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 9, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 9, 2024
@faenuccio
style(DedekindDomain/AdicValuation): fix some snake_case to lowerCame…
e90957e 
…lCase (#14533)

In some theorem names, `int_valuation`  was still used instead of `intValuation`, and this PR fixes this.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 9, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title style(DedekindDomain/AdicValuation): fix some snake_case to lowerCamelCase [Merged by Bors] - style(DedekindDomain/AdicValuation): fix some snake_case to lowerCamelCase Jul 9, 2024
@mathlib-bors mathlib-bors bot closed this Jul 9, 2024
@mathlib-bors mathlib-bors bot deleted the fae_PR_lowerCamelCase_adicCompletion branch July 9, 2024 14:20
@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

No reviews

Assignees

@mariainesdff mariainesdff

Labels

easy < 20s of review time. See the lifecycle page for guidelines. maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. 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.

6 participants

@faenuccio @grunweg @adomani @mariainesdff @riccardobrasca @kim-em