Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#6289)
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 Feb 18, 2021
1 parent 7592a8f commit 7c267df
Showing 1 changed file with 32 additions and 42 deletions.
74 changes: 32 additions & 42 deletions scripts/style-exceptions.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,8 @@ src/analysis/normed_space/bounded_linear_maps.lean : line 148 : ERR_LIN : Line h
src/analysis/normed_space/bounded_linear_maps.lean : line 254 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/bounded_linear_maps.lean : line 377 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/bounded_linear_maps.lean : line 421 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 722 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 942 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 1015 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 735 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 1149 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 1151 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 1152 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -379,8 +379,8 @@ src/data/seq/computation.lean : line 11 : ERR_MOD : Module docstring missing, or
src/data/seq/parallel.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/data/seq/seq.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/seq/wseq.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/set/basic.lean : line 2333 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 880 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 2337 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 884 : ERR_LIN : Line has more than 100 characters
src/data/set/countable.lean : line 143 : ERR_LIN : Line has more than 100 characters
src/data/set/countable.lean : line 159 : ERR_LIN : Line has more than 100 characters
src/data/set/disjointed.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Expand All @@ -400,8 +400,7 @@ src/data/sym2.lean : line 173 : ERR_LIN : Line has more than 100 characters
src/data/sym2.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/ulift.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/vector2.lean : line 334 : ERR_LIN : Line has more than 100 characters
src/data/vector2.lean : line 339 : ERR_LIN : Line has more than 100 characters
src/data/vector2.lean : line 368 : ERR_LIN : Line has more than 100 characters
src/data/vector2.lean : line 357 : ERR_LIN : Line has more than 100 characters
src/data/zmod/basic.lean : line 360 : ERR_LIN : Line has more than 100 characters
src/data/zsqrtd/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/deprecated/subfield.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -485,9 +484,9 @@ src/group_theory/presented_group.lean : line 11 : ERR_MOD : Module docstring mis
src/group_theory/presented_group.lean : line 51 : ERR_LIN : Line has more than 100 characters
src/group_theory/quotient_group.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/group_theory/semidirect_product.lean : line 52 : ERR_LIN : Line has more than 100 characters
src/group_theory/subgroup.lean : line 386 : ERR_LIN : Line has more than 100 characters
src/group_theory/subgroup.lean : line 854 : ERR_LIN : Line has more than 100 characters
src/group_theory/subgroup.lean : line 889 : ERR_LIN : Line has more than 100 characters
src/group_theory/subgroup.lean : line 400 : ERR_LIN : Line has more than 100 characters
src/group_theory/subgroup.lean : line 876 : ERR_LIN : Line has more than 100 characters
src/group_theory/subgroup.lean : line 911 : ERR_LIN : Line has more than 100 characters
src/group_theory/submonoid/operations.lean : line 560 : ERR_LIN : Line has more than 100 characters
src/group_theory/sylow.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/linear_algebra/basis.lean : line 292 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -599,26 +598,26 @@ src/ring_theory/free_comm_ring.lean : line 262 : ERR_LIN : Line has more than 10
src/ring_theory/free_comm_ring.lean : line 264 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 266 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/basic.lean : line 58 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 1269 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 1272 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 140 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 1408 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 144 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 1007 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 1278 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 1281 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 141 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 1417 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 145 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 304 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 322 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 376 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 438 : 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 443 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 444 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 547 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 570 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 867 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 95 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 97 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 998 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 146 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 310 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 328 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 390 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 452 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 455 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 456 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 457 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 458 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 556 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 579 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 876 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 96 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 98 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_closure.lean : line 119 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_closure.lean : line 124 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_closure.lean : line 209 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -658,12 +657,12 @@ src/ring_theory/polynomial/scale_roots.lean : line 92 : ERR_LIN : Line has more
src/ring_theory/principal_ideal_domain.lean : line 121 : ERR_LIN : Line has more than 100 characters
src/ring_theory/principal_ideal_domain.lean : line 124 : ERR_LIN : Line has more than 100 characters
src/ring_theory/roots_of_unity.lean : line 150 : ERR_LIN : Line has more than 100 characters
src/ring_theory/subring.lean : line 413 : ERR_LIN : Line has more than 100 characters
src/ring_theory/subring.lean : line 420 : ERR_LIN : Line has more than 100 characters
src/ring_theory/subring.lean : line 464 : ERR_LIN : Line has more than 100 characters
src/ring_theory/subring.lean : line 410 : ERR_LIN : Line has more than 100 characters
src/ring_theory/subring.lean : line 417 : ERR_LIN : Line has more than 100 characters
src/ring_theory/subring.lean : line 461 : ERR_LIN : Line has more than 100 characters
src/ring_theory/subring.lean : line 483 : ERR_LIN : Line has more than 100 characters
src/ring_theory/subring.lean : line 486 : ERR_LIN : Line has more than 100 characters
src/ring_theory/subring.lean : line 489 : ERR_LIN : Line has more than 100 characters
src/ring_theory/subring.lean : line 748 : ERR_LIN : Line has more than 100 characters
src/ring_theory/subring.lean : line 770 : ERR_LIN : Line has more than 100 characters
src/ring_theory/tensor_product.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/ring_theory/tensor_product.lean : line 489 : ERR_LIN : Line has more than 100 characters
src/ring_theory/unique_factorization_domain.lean : line 11 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -948,15 +947,6 @@ src/topology/sheaves/sheaf.lean : line 89 : ERR_LIN : Line has more than 100 cha
src/topology/sheaves/sheaf.lean : line 91 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf_condition/equalizer_products.lean : line 230 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf_condition/equalizer_products.lean : line 231 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf_condition/pairwise_intersections.lean : line 102 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf_condition/pairwise_intersections.lean : line 106 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf_condition/pairwise_intersections.lean : line 111 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf_condition/pairwise_intersections.lean : line 116 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf_condition/pairwise_intersections.lean : line 281 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf_condition/pairwise_intersections.lean : line 294 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf_condition/pairwise_intersections.lean : line 315 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf_condition/pairwise_intersections.lean : line 326 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf_condition/pairwise_intersections.lean : line 55 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf_of_functions.lean : line 168 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/stalks.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/topology/sheaves/stalks.lean : line 128 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 7c267df

Please sign in to comment.