grunweg
grunweg
!bench
@kmill Thanks for commenting about the `GeneralizeProofs` change; I'm learning something new every day! The linter ignores `partial` declarations now; I just verified that the change *could* be reverted. Would...
It was [on a dependent PR](https://github.com/leanprover-community/mathlib4/pull/17125#issuecomment-2405497324).
I'm also open to reverting [this commit](https://github.com/leanprover-community/mathlib4/pull/10235/commits/4b1e329abaf49f0fcf8aa6fab48096effdaf9034), or rather, just the second half. (The first half is fine now.)
@kmill Thanks for the explanations. I had tried `isPartial`, but that did not do what I wanted (or did not go far enough?). I've tried to check for `opaqueInfo` now;...
:bulb: That is helpful. Would you like to file PR adding this docstring? Or should I create one, so you can get help fixing it more easily :-)?
!bench
I'm happy with merging it, and looking at post-merge benchmarking output.
I am not confident there will be no regression in linting times - but as there are further such linters in the pipeline, I am not worried about that item...
Thanks for the fixes; they look good to me.