grunweg

Results 112 comments of grunweg

refactor: `reduceOption_length_le`

Did you PR just the code movement separately? (I could've sworn I saw this somewhere...) I'd approve (I don't have review rights) such a PR quickly, and it might speed...

chore(Order/Intervals/Set): move some defs to a new file

Thanks! maintainer merge

chore(Order/Intervals/Set): move some defs to a new file

(CI fails because of a linter warning: I just pushed a trivial fix.)

feat: Shake autodetects which module(s) to shake

My understanding is that the equivalent PR has landed in mathlib, so this PR can be closed. (If shake were to be upstreamed to batteries, #1204 should be updated.) That...

chore(TwoSidedIdeal/Basic): fix docs string

Thanks for following up! I have just one tiny question; would `maintainer merge` with that addressed. Did you think about this part of `jcommelin`'s comment? > Then you can use...

chore(TwoSidedIdeal/Basic): fix docs string

Thanks! maintainer merge

feat(LinearAlgebra/CliffordAlgebra): port SpinGroup

Drive-by comment: is this awaiting review? Then it would help to label it as such, otherwise this may slip through the queue. :-)

feat: the unusedVariableCommand linter

Adding this for reference: I presume the new async linting also confuses the linter, so would have to be turned off as well, right? See #20755 for reference.

rename: `no_lost_declarations` to `decls_diff` and `short` as default option

Looks reasonable! What do you think about renaming to `declarations_diff`? (I find the latter more *readable*; if mostly CI runs this, one might as well use a readable name.) Feel...

rename: `no_lost_declarations` to `decls_diff` and `short` as default option

Thanks! maintainer merge