Skip to content

Commit 35029c2

Browse files
chore(scripts): update nolints.json (leanprover-community#35618)
I am happy to remove some nolints for you!
1 parent f50fac7 commit 35029c2

1 file changed

Lines changed: 3 additions & 6 deletions

File tree

scripts/nolints.json

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -55,9 +55,6 @@
5555
["docBlame", "LinearPMap.sSup"],
5656
["docBlame", "LinearPMap.toFun"],
5757
["docBlame", "LinearPMap.toFun'"],
58-
["docBlame", "Lists.Equiv.decidable"],
59-
["docBlame", "Lists.Subset.decidable"],
60-
["docBlame", "Lists.mem.decidable"],
6158
["docBlame", "MaximalSpectrum.asIdeal"],
6259
["docBlame", "ModularForm.«term_∣[_]_»"],
6360
["docBlame", "MonadCont.Label"],
@@ -86,7 +83,6 @@
8683
["docBlame", "RingQuot.preLift"],
8784
["docBlame", "RingQuot.preLiftAlgHom"],
8885
["docBlame", "RingQuot.toQuot"],
89-
["docBlame", "SetTheory.PGame.shortAdd"],
9086
["docBlame", "Shrink.rec"],
9187
["docBlame", "SlashAction.map"],
9288
["docBlame", "StarAlgEquiv.restrictScalars"],
@@ -166,6 +162,9 @@
166162
["docBlame", "Lean.MVarId.congrCore!"],
167163
["docBlame", "Lean.Name.isBlackListed"],
168164
["docBlame", "Lean.PHashSet.toList"],
165+
["docBlame", "Lists.Equiv.decidable"],
166+
["docBlame", "Lists.Subset.decidable"],
167+
["docBlame", "Lists.mem.decidable"],
169168
["docBlame", "LocallyFinite.Realizer.bas"],
170169
["docBlame", "LocallyFinite.Realizer.sets"],
171170
["docBlame", "Mathlib.Notation3.expandFoldl"],
@@ -228,8 +227,6 @@
228227
["docBlame", "Module.End.Eigenvalues.val"],
229228
["docBlame", "Order.Ideal.PrimePair.F"],
230229
["docBlame", "Order.Ideal.PrimePair.I"],
231-
["docBlame", "Lean.Meta.mkRichHCongr.doubleTelescope.loop"],
232-
["docBlame", "Lean.Meta.mkRichHCongr.withNewEqs.loop"],
233230
["docBlame", "Mathlib.Command.Variable.variable?.checkRedundant"],
234231
["docBlame", "Mathlib.Command.Variable.variable?.maxSteps"],
235232
["docBlame", "Mathlib.Tactic.Coherence.LiftHom.lift"],

0 commit comments

Comments
 (0)