-
Notifications
You must be signed in to change notification settings - Fork 299
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(set_theory/cardinal/basic): improve docs on lift
, add simp
lemmas
#14596
Conversation
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.
The PR description claims this adds documentation to lift
, but it doesn't; did you forget to commit that documentation?
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 would be great if we could teach the pretty-printer to handle this; perhaps with an @[pp_universes]
attribute on lift
.
Perhaps @kmill has some ideas here.
I didn't change the docs on |
This reverts commit 7f546ea.
Sorry, wrong PR. |
bors merge |
…emmas (#14596) We add some much needed documentation to the `cardinal.lift` API. We also mark a few extra lemmas with `simp`.
Build failed (retrying...): |
…emmas (#14596) We add some much needed documentation to the `cardinal.lift` API. We also mark a few extra lemmas with `simp`.
Pull request successfully merged into master. Build succeeded: |
lift
, add simp
lemmaslift
, add simp
lemmas
We add some much needed documentation to the
cardinal.lift
API. We also mark a few extra lemmas withsimp
.