-
Notifications
You must be signed in to change notification settings - Fork 256
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] - feat: port Mathlib.Data.Real.CauSeqCompletion #1440
Conversation
…o mcdoll/data_real_causeq
…o mcdoll/data_real_causeq
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
Perhaps we should remove the |
This is good now except for the |
LGTM! But Heather's suggestion is still open. |
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.
Thanks 🎉
bors merge
- [x] depends on: #1124 This is quite painful due to `parameter` use in mathlib3. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded:
|
This reverts commit 0a713e2. The motivation is to allow leanprover-community/mathlib#18122 to generate pre-port mathport output in the mathlib3port CI. Once that is done, I will unrevert this and merge in the changes it suggests.
This reverts commit 0a713e2. The motivation is to allow leanprover-community/mathlib#18122 to generate pre-port mathport output in the mathlib3port CI. Once that is done, I will unrevert this and merge in the changes it suggests.
Unreverts #1440 Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
- [x] depends on: #1124 This is quite painful due to `parameter` use in mathlib3. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
This reverts commit 0a713e2. The motivation is to allow leanprover-community/mathlib#18122 to generate pre-port mathport output in the mathlib3port CI. Once that is done, I will unrevert this and merge in the changes it suggests.
Unreverts #1440 Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
This is quite painful due to
parameter
use in mathlib3.