Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

refactor: change notation for interval integrals #19225

Closed
wants to merge 4 commits into from
Closed

refactor: change notation for interval integrals #19225

wants to merge 4 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Jun 30, 2023

Open in Gitpod

@urkud urkud added RFC Request for comment awaiting-review The author would like community review of the PR labels Jun 30, 2023
@urkud urkud requested review from a team as code owners June 30, 2023 15:41
@github-actions github-actions bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Jun 30, 2023
@eric-wieser eric-wieser added the not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 label Jul 15, 2023
@urkud urkud added too-late This PR was ready too late for inclusion in mathlib3 and removed not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 labels Jul 16, 2023
@urkud
Copy link
Member Author

urkud commented Jul 16, 2023

Changed to too-late because I failed to find a new notation that (a) will be accepted by the community; (b) works well both in Lean 3 and Lean 4.

@urkud
Copy link
Member Author

urkud commented Jun 20, 2024

Even if we'll decide to change notation in Lean 4, it no longer makes sense to change it in Lean 3 too.

@urkud urkud closed this Jun 20, 2024
@urkud urkud deleted the YK-interval-integral branch June 20, 2024 04:06
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-review The author would like community review of the PR modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. RFC Request for comment too-late This PR was ready too late for inclusion in mathlib3
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@urkud @eric-wieser