-
Notifications
You must be signed in to change notification settings - Fork 265
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.
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
[Merged by Bors] - chore: resolve (coe : ℤ → α) to ((↑) : ℤ → α)
porting notes
#11250
Conversation
Let's just fix these; all the |
@eric-wieser Fixed and edited the issue and PR titles. |
(coe : ℤ → α) to (Int.cast : ℤ → α)
porting notes(coe : ℤ → α) to ((↑) : ℤ → α)
porting notes
-- Porting note: changed `(coe : ℤ → α)` to `(Int.cast : ℤ → α)` | ||
theorem gc_coe_floor : GaloisConnection (Int.cast : ℤ → α) floor := | ||
theorem gc_coe_floor : GaloisConnection ((↑) : ℤ → α) floor := | ||
FloorRing.gc_coe_floor | ||
#align int.gc_coe_floor Int.gc_coe_floor |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@YaelDillies, do you know why we have both Int.gc_coe_floor
and FloorRing.gc_coe_floor
? Was one about a different coercion in mathlib3?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it was just for discoverability as the operator is Int.floor
, not FloorRing.floor
.
(coe : ℤ → α) to ((↑) : ℤ → α)
porting notes(coe : ℤ → α) to ((↑) : ℤ → α)
porting notes
bors d=@YaelDillies |
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
Why not just remove the porting notes? |
Hi @YaelDillies, I’ve removed them and updated title and description. |
No, that's not what I meant. I meant "Why are you replacing |
@YaelDillies, I don't understand your comment, it seems to be talking about a patch that doesn't exist in this PR. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh I see I swapped the diff colors in my head 🙈
bors merge
Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.
Pull request successfully merged into master. Build succeeded: |
(coe : ℤ → α) to ((↑) : ℤ → α)
porting notes(coe : ℤ → α) to ((↑) : ℤ → α)
porting notes
Closes #11249 |
Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.
Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.
Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.
Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.
Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.
Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.
Resolves porting notes claiming "change
(coe : ℤ → α)
to((↑) : ℤ → α)
" by substitutingInt.cast
with(↑)
.