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] - chore: Remove Init.Propext
#10709
Conversation
These lemmas can easily go to `Logic.Basic`
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.
Looks plausible to me.
Mathlib/Logic/Basic.lean
Outdated
/-- Alias of `propext`. -/ | ||
lemma Iff.eq : (a ↔ b) → a = b := propext |
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.
/-- Alias of `propext`. -/ | |
lemma Iff.eq : (a ↔ b) → a = b := propext | |
alias Iff.eq := propext |
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.
I can't because alias
is not imported there. Should I import it?
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.
yes
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.
Nevermind, it is? 🤔
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.
Sorry I remember the problem: alias
creates def Iff.eq := propext
, not lemma Iff.eq := propext
. Will nolint for now.
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 shouldn't? Report it as a bug if so
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's supposed to create defs from defs and theorems from theorems, but you are aliasing an axiom
and I guess these can be either defs or theorems
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 🎉
If CI passes, please remove the label awaiting-CI
and merge this yourself, by adding a comment bors r+
.
bors d+
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
These lemmas can easily go to `Logic.Basic`
Pull request successfully merged into master. Build succeeded: |
Init.Propext
Init.Propext
These lemmas can easily go to `Logic.Basic`
These lemmas can easily go to `Logic.Basic`
These lemmas can easily go to `Logic.Basic`
These lemmas can easily go to `Logic.Basic`
These lemmas can easily go to
Logic.Basic