-
Notifications
You must be signed in to change notification settings - Fork 314
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 SetTheory.Ordinal.Notation #2470
Conversation
mo271
commented
Feb 23, 2023
•
edited by github-actions
bot
Loading
edited by github-actions
bot
- depends on: [Merged by Bors] - feat: port Init.Data.Ordering.Lemmas #4281
9f18380
to
6908018
Compare
I just rebased this to the newest master, but I don't actually manage to make any progress :( |
I'll make an attempt to clean up the Mathlib 3 file. Hopefully that helps porting this file. |
6908018
to
da3d246
Compare
This PR/issue depends on:
|
da3d246
to
5ad4141
Compare
Any news, @vihdzp ? |
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
open Ordinal Order | ||
|
||
open Ordinal | ||
|
||
-- Porting note: the generated theorem gets lint. | ||
set_option genSizeOfSpec false in | ||
-- get notation for `ω` |
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.
open Ordinal Order | |
open Ordinal | |
-- Porting note: the generated theorem gets lint. | |
set_option genSizeOfSpec false in | |
-- get notation for `ω` | |
open Ordinal Order | |
-- Porting note: the generated theorem gets lint. | |
set_option genSizeOfSpec false in |
The mathlib3 source had
open ordinal order
open_locale ordinal -- get notation for `ω`
that's where the comment comes from
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.
It seems the comment has now vanished from the source. Could it be restored, please?
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.
Even without the notation for ω
, open Ordinal
is required.
And, in Lean 4, when an namespace is opened, its locale is automatically opened too, so open_locale ordinal
and the comment is not needed anymore.
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, sorry to be slow.
bors merge |
Co-authored-by: Arien Malec <arien.malec@gmail.com> Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Jon Eugster <eugster.jon@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Apurva Nakade <apurvnakade@gmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Co-authored-by: Arien Malec <arien.malec@gmail.com> Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Jon Eugster <eugster.jon@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Apurva Nakade <apurvnakade@gmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Arien Malec <arien.malec@gmail.com> Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Jon Eugster <eugster.jon@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Apurva Nakade <apurvnakade@gmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Arien Malec <arien.malec@gmail.com> Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Jon Eugster <eugster.jon@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Apurva Nakade <apurvnakade@gmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Arien Malec <arien.malec@gmail.com> Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Jon Eugster <eugster.jon@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Apurva Nakade <apurvnakade@gmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp>