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] - fix(*): mark some classes as Prop #18015
Conversation
urkud
commented
Dec 26, 2022
Looks good, thanks! One file has been ported to mathlib4; do those classes already live in Prop in Lean 4? If yes then no matching PR is needed, but I guess mathport checks universes as well and the answer is no. I also spotted two other examples previously; would you include them 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.
Thanks!
maintainer merge
The matching PR is not yet approved but the plan seems to be merging this first
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
Thanks 🎉 bors merge |
Pull request successfully merged into master. Build succeeded: |
Also make `SubmonoidClass` extend `OneMemClass`. This is a Lean 4 version of leanprover-community/mathlib#18015
Also make `SubmonoidClass` extend `OneMemClass`. This is a Lean 4 version of leanprover-community/mathlib#18015 Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>