Skip to content

[Merged by Bors] - chore(Data/Rat/Cast/Order): Use p, q as variable names#13644

Closed
YaelDillies wants to merge 3 commits intomasterfrom
rat_cast_order_variable_names
Closed

[Merged by Bors] - chore(Data/Rat/Cast/Order): Use p, q as variable names#13644
YaelDillies wants to merge 3 commits intomasterfrom
rat_cast_order_variable_names

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Jun 8, 2024

... rather than a, b, m, n, r. Also make arguments to rewriting lemmas explicit.

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jun 8, 2024
@github-actions
Copy link
Copy Markdown

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

PR summary

Import changes

No significant changes to the import graph

Declarations diff

++-- cast_le
++-- cast_lt
++-- cast_lt_zero
++-- cast_max
++-- cast_min
++-- cast_nonpos
++-- cast_pos
-+-+ cast_strictMono
--++ preimage_cast_Icc
--++ preimage_cast_Ici
--++ preimage_cast_Ico
--++ preimage_cast_Iic
--++ preimage_cast_Iio
--++ preimage_cast_Ioc
--++ preimage_cast_Ioi
--++ preimage_cast_Ioo
--++ preimage_cast_uIcc
--++ preimage_cast_uIoc

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>

@YaelDillies YaelDillies mentioned this pull request Jun 8, 2024
Closed
eric-wieser
eric-wieser approved these changes Jun 8, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

bors d+

CI is unhappy

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 8, 2024

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

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jun 8, 2024
eric-wieser
eric-wieser reviewed Jun 8, 2024
View reviewed changes
@YaelDillies YaelDillies added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Jun 9, 2024
@YaelDillies
chore(Data/Rat/Cast/Order): Use p, q as variable names
f8812da 
... rather than `a`, `b`, `m`, `n`, `r`. Also make arguments to rewriting lemmas explicit.
@YaelDillies
more
643cd93
@YaelDillies YaelDillies force-pushed the rat_cast_order_variable_names branch from 2c46893 to 643cd93 Compare June 9, 2024 09:59
@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 Jun 9, 2024
@ghost
Copy link
Copy Markdown

ghost commented Jun 9, 2024

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Jun 9, 2024
@YaelDillies
chore(Data/Rat/Cast/Order): Use p, q as variable names (#13644)
d35039b 
... rather than `a`, `b`, `m`, `n`, `r`. Also make arguments to rewriting lemmas explicit.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 9, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Data/Rat/Cast/Order): Use p, q as variable names [Merged by Bors] - chore(Data/Rat/Cast/Order): Use p, q as variable names Jun 9, 2024
@mathlib-bors mathlib-bors bot closed this Jun 9, 2024
@mathlib-bors mathlib-bors bot deleted the rat_cast_order_variable_names branch June 9, 2024 12:53
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@YaelDillies @AntoineChambert-Loir
chore(Data/Rat/Cast/Order): Use p, q as variable names (#13644)
12cbd6f 
... rather than `a`, `b`, `m`, `n`, `r`. Also make arguments to rewriting lemmas explicit.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees

No one assigned

Labels

auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer).

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@YaelDillies @eric-wieser