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 Data.Matrix.PEquiv #3234
Conversation
Ruben-VandeVelde
commented
Apr 2, 2023
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
Mathlib/Data/Matrix/PEquiv.lean
Outdated
instance [DecidableEq n] (j : n) (o : Option n) : Decidable (j ∈ o) := by | ||
rw [←Option.mem_toList] | ||
infer_instance |
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.
This instance shouldn't need [DecidableEq n]
What instance is found in Lean3?
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.
option.decidable_eq
Mathlib/Data/Matrix/PEquiv.lean
Outdated
-- Porting note: added | ||
local instance [DecidableEq n] (j : n) (o : Option n) : Decidable (j ∈ o) := | ||
haveI : Decidable (o = some j) := inferInstance | ||
this |
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.
This is definitely better, but belongs in the same file that defines the ∈
notation
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.
That's Std.Data.Option.Basic. I'll submit a PR there tomorrow, but wouldn't mind if we moved this along in the meantime.
bors merge |
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>