Conversation
|
|
||
| theorem H₄IsCoxeter : IsCoxeter H₄ where | ||
| symmetric := by simp [Matrix.IsSymm]; decide | ||
| symmetric := by unfold Matrix.IsSymm; decide |
There was a problem hiding this comment.
I guess these could have been simp with decide turned on instead? I'm a bit wary of these. Decide is a good example of a tactic that doesn't card too much what the goal is before but might run a lot slower if the input is in a different form
|
|
||
| theorem G₂IsCoxeter : IsCoxeter G₂ where | ||
| symmetric := by simp [Matrix.IsSymm]; decide | ||
| symmetric := by unfold Matrix.IsSymm; decide |
There was a problem hiding this comment.
If you add an instance for DecidablePred Matrix.IsSymm (which should be pretty trivial), you will be able to golf this even further to
| symmetric := by unfold Matrix.IsSymm; decide | |
| symmetric := by decide |
adomani
left a comment
There was a problem hiding this comment.
Thanks for the reviews! I am skeptical about adding the Decidable instance for Matrix.IsSymm in the same PR.
Also, these issues are still using the old linter. I have not yet had the time to really think through the new one, though.
|
!bench |
|
Here are the benchmark results for commit 6cde597. |
|
Same as in #11281: I understood that the implementation of the "flexible linter" addresses this PR and therefore this can be closed. Please reopen if that's not correct! |
One more PR with
simps squeezed thanks to #11246.