Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5652)
Browse files Browse the repository at this point in the history 
I am happy to remove some nolints for you!
  • Loading branch information
@leanprover-community-bot
leanprover-community-bot committed Jan 7, 2021
1 parent f668be0 commit 3f35961
Showing 1 changed file with 21 additions and 23 deletions.
44 changes: 21 additions & 23 deletions scripts/style-exceptions.txt
View file
Expand Up @@ -93,13 +93,13 @@ src/algebra/invertible.lean : line 216 : ERR_LIN : Line has more than 100 charac
src/algebra/invertible.lean : line 224 : ERR_LIN : Line has more than 100 characters
src/algebra/invertible.lean : line 233 : ERR_LIN : Line has more than 100 characters
src/algebra/invertible.lean : line 84 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 1069 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 1250 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 241 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 245 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 385 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 68 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 83 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 1075 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 1256 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 231 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 235 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 375 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 58 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 73 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/classical.lean : line 124 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/classical.lean : line 215 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/classical.lean : line 363 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -753,11 +753,12 @@ src/data/mv_polynomial/basic.lean : line 509 : ERR_LIN : Line has more than 100
src/data/mv_polynomial/basic.lean : line 814 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/comm_ring.lean : line 113 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/counit.lean : line 19 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/equiv.lean : line 104 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/equiv.lean : line 114 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/equiv.lean : line 106 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/equiv.lean : line 116 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/equiv.lean : line 250 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/equiv.lean : line 94 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/equiv.lean : line 126 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/equiv.lean : line 128 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/equiv.lean : line 262 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/equiv.lean : line 66 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/invertible.lean : line 13 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/invertible.lean : line 23 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/monad.lean : line 197 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -828,7 +829,7 @@ src/data/padics/padic_numbers.lean : line 14 : ERR_LIN : Line has more than 100
src/data/padics/padic_numbers.lean : line 32 : ERR_LIN : Line has more than 100 characters
src/data/padics/padic_numbers.lean : line 40 : ERR_LIN : Line has more than 100 characters
src/data/padics/padic_numbers.lean : line 870 : ERR_LIN : Line has more than 100 characters
src/data/padics/ring_homs.lean : line 640 : ERR_LIN : Line has more than 100 characters
src/data/padics/ring_homs.lean : line 638 : ERR_LIN : Line has more than 100 characters
src/data/pequiv.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/pfun.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/pfunctor/multivariate/M.lean : line 43 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1129,7 +1130,7 @@ src/logic/relation.lean : line 10 : ERR_MOD : Module docstring missing, or too l
src/logic/relator.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/measure_theory/category/Meas.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/measure_theory/decomposition.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/measure_theory/measure_space.lean : line 1729 : ERR_LIN : Line has more than 100 characters
src/measure_theory/measure_space.lean : line 1760 : ERR_LIN : Line has more than 100 characters
src/measure_theory/measure_space.lean : line 65 : ERR_LIN : Line has more than 100 characters
src/meta/coinductive_predicates.lean : line 115 : ERR_LIN : Line has more than 100 characters
src/meta/coinductive_predicates.lean : line 12 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1286,11 +1287,7 @@ src/order/zorn.lean : line 241 : ERR_LIN : Line has more than 100 characters
src/order/zorn.lean : line 47 : ERR_LIN : Line has more than 100 characters
src/ring_theory/algebra_tower.lean : line 103 : ERR_LIN : Line has more than 100 characters
src/ring_theory/algebra_tower.lean : line 219 : ERR_LIN : Line has more than 100 characters
src/ring_theory/dedekind_domain.lean : line 112 : ERR_LIN : Line has more than 100 characters
src/ring_theory/dedekind_domain.lean : line 21 : ERR_LIN : Line has more than 100 characters
src/ring_theory/dedekind_domain.lean : line 23 : ERR_LIN : Line has more than 100 characters
src/ring_theory/dedekind_domain.lean : line 25 : ERR_LIN : Line has more than 100 characters
src/ring_theory/dedekind_domain.lean : line 84 : ERR_LIN : Line has more than 100 characters
src/ring_theory/derivation.lean : line 207 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 109 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 112 : ERR_LIN : Line has more than 100 characters
Expand All @@ -1303,7 +1300,7 @@ src/ring_theory/free_comm_ring.lean : line 261 : ERR_LIN : Line has more than 10
src/ring_theory/free_comm_ring.lean : line 263 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_ring.lean : line 83 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_ring.lean : line 86 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/basic.lean : line 59 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/basic.lean : line 63 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 1264 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 138 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 142 : ERR_LIN : Line has more than 100 characters
Expand All @@ -1315,6 +1312,7 @@ src/ring_theory/ideal/operations.lean : line 436 : ERR_LIN : Line has more than
src/ring_theory/ideal/operations.lean : line 439 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 440 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 441 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 442 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 46 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 545 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 568 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1353,11 +1351,11 @@ src/ring_theory/multiplicity.lean : line 10 : ERR_MOD : Module docstring missing
src/ring_theory/multiplicity.lean : line 313 : ERR_LIN : Line has more than 100 characters
src/ring_theory/multiplicity.lean : line 314 : ERR_LIN : Line has more than 100 characters
src/ring_theory/noetherian.lean : line 178 : ERR_LIN : Line has more than 100 characters
src/ring_theory/noetherian.lean : line 372 : ERR_LIN : Line has more than 100 characters
src/ring_theory/noetherian.lean : line 392 : ERR_LIN : Line has more than 100 characters
src/ring_theory/noetherian.lean : line 394 : ERR_LIN : Line has more than 100 characters
src/ring_theory/noetherian.lean : line 561 : ERR_LIN : Line has more than 100 characters
src/ring_theory/noetherian.lean : line 565 : ERR_LIN : Line has more than 100 characters
src/ring_theory/noetherian.lean : line 371 : ERR_LIN : Line has more than 100 characters
src/ring_theory/noetherian.lean : line 391 : ERR_LIN : Line has more than 100 characters
src/ring_theory/noetherian.lean : line 393 : ERR_LIN : Line has more than 100 characters
src/ring_theory/noetherian.lean : line 560 : ERR_LIN : Line has more than 100 characters
src/ring_theory/noetherian.lean : line 564 : ERR_LIN : Line has more than 100 characters
src/ring_theory/polynomial/basic.lean : line 135 : ERR_LIN : Line has more than 100 characters
src/ring_theory/polynomial/basic.lean : line 137 : ERR_LIN : Line has more than 100 characters
src/ring_theory/polynomial/basic.lean : line 147 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 3f35961

Please sign in to comment.