Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5048)
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 Nov 20, 2020
1 parent 47542a0 commit 0e976d9
Showing 1 changed file with 24 additions and 27 deletions.
51 changes: 24 additions & 27 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -91,7 +91,7 @@ src/algebra/free_algebra.lean : line 277 : ERR_LIN : Line has more than 100 char
src/algebra/free_algebra.lean : line 279 : ERR_LIN : Line has more than 100 characters
src/algebra/free_algebra.lean : line 323 : ERR_LIN : Line has more than 100 characters
src/algebra/free_algebra.lean : line 36 : ERR_LIN : Line has more than 100 characters
src/algebra/free_monoid.lean : line 55 : ERR_LIN : Line has more than 100 characters
src/algebra/free_monoid.lean : line 59 : ERR_LIN : Line has more than 100 characters
src/algebra/geom_sum.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/algebra/group/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/algebra/group/defs.lean : line 288 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -128,11 +128,11 @@ src/algebra/module/ordered.lean : line 192 : ERR_LIN : Line has more than 100 ch
src/algebra/module/pi.lean : line 63 : ERR_LIN : Line has more than 100 characters
src/algebra/module/pi.lean : line 77 : ERR_LIN : Line has more than 100 characters
src/algebra/module/submodule.lean : line 13 : ERR_LIN : Line has more than 100 characters
src/algebra/monoid_algebra.lean : line 624 : ERR_LIN : Line has more than 100 characters
src/algebra/monoid_algebra.lean : line 768 : ERR_LIN : Line has more than 100 characters
src/algebra/monoid_algebra.lean : line 824 : ERR_LIN : Line has more than 100 characters
src/algebra/monoid_algebra.lean : line 833 : ERR_LIN : Line has more than 100 characters
src/algebra/monoid_algebra.lean : line 844 : ERR_LIN : Line has more than 100 characters
src/algebra/monoid_algebra.lean : line 627 : ERR_LIN : Line has more than 100 characters
src/algebra/monoid_algebra.lean : line 774 : ERR_LIN : Line has more than 100 characters
src/algebra/monoid_algebra.lean : line 830 : ERR_LIN : Line has more than 100 characters
src/algebra/monoid_algebra.lean : line 839 : ERR_LIN : Line has more than 100 characters
src/algebra/monoid_algebra.lean : line 850 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_group.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/algebra/ordered_group.lean : line 1230 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_group.lean : line 1232 : ERR_LIN : Line has more than 100 characters
Expand All @@ -144,7 +144,7 @@ src/algebra/quandle.lean : line 462 : ERR_LIN : Line has more than 100 character
src/algebra/quandle.lean : line 66 : ERR_LIN : Line has more than 100 characters
src/algebra/quandle.lean : line 67 : ERR_LIN : Line has more than 100 characters
src/algebra/ring/pi.lean : line 67 : ERR_LIN : Line has more than 100 characters
src/algebra/ring_quot.lean : line 278 : ERR_LIN : Line has more than 100 characters
src/algebra/ring_quot.lean : line 293 : ERR_LIN : Line has more than 100 characters
src/algebra/ring_quot.lean : line 46 : ERR_LIN : Line has more than 100 characters
src/algebraic_geometry/Scheme.lean : line 29 : ERR_LIN : Line has more than 100 characters
src/algebraic_geometry/locally_ringed_space.lean : line 18 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -253,10 +253,10 @@ src/analysis/normed_space/operator_norm.lean : line 34 : ERR_LIN : Line has more
src/analysis/normed_space/operator_norm.lean : line 628 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 87 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/arsinh.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/analysis/special_functions/pow.lean : line 1344 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 294 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 1338 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 295 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 547 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 296 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 548 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1109 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1123 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1126 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -783,17 +783,17 @@ src/data/matrix/pequiv.lean : line 137 : ERR_LIN : Line has more than 100 charac
src/data/matrix/pequiv.lean : line 143 : ERR_LIN : Line has more than 100 characters
src/data/matrix/pequiv.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/mllist.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/data/multiset/basic.lean : line 1028 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1035 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 116 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 128 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1282 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1289 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 133 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1720 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1729 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1745 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1748 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1926 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 2050 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1727 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1736 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1752 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1755 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1944 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 2068 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 542 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 666 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 677 : ERR_LIN : Line has more than 100 characters
Expand All @@ -802,7 +802,7 @@ src/data/multiset/basic.lean : line 704 : ERR_LIN : Line has more than 100 chara
src/data/multiset/basic.lean : line 707 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 719 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 722 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 965 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 972 : ERR_LIN : Line has more than 100 characters
src/data/multiset/fold.lean : line 25 : ERR_LIN : Line has more than 100 characters
src/data/multiset/fold.lean : line 32 : ERR_LIN : Line has more than 100 characters
src/data/multiset/fold.lean : line 49 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1009,20 +1009,17 @@ src/field_theory/fixed.lean : line 27 : ERR_LIN : Line has more than 100 charact
src/field_theory/fixed.lean : line 77 : ERR_LIN : Line has more than 100 characters
src/field_theory/intermediate_field.lean : line 150 : ERR_LIN : Line has more than 100 characters
src/field_theory/intermediate_field.lean : line 155 : ERR_LIN : Line has more than 100 characters
src/field_theory/minimal_polynomial.lean : line 116 : ERR_LIN : Line has more than 100 characters
src/field_theory/minimal_polynomial.lean : line 214 : ERR_LIN : Line has more than 100 characters
src/field_theory/mv_polynomial.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/field_theory/primitive_element.lean : line 29 : ERR_LIN : Line has more than 100 characters
src/field_theory/separable.lean : line 219 : ERR_LIN : Line has more than 100 characters
src/field_theory/separable.lean : line 404 : ERR_LIN : Line has more than 100 characters
src/field_theory/separable.lean : line 523 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 15 : ERR_MOD : Module docstring missing, or too late
src/field_theory/splitting_field.lean : line 374 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 376 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 379 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 436 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 485 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 500 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 576 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 486 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 501 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 577 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 76 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 77 : ERR_LIN : Line has more than 100 characters
src/field_theory/subfield.lean : line 449 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1472,7 +1469,7 @@ src/ring_theory/unique_factorization_domain.lean : line 111 : ERR_LIN : Line has
src/ring_theory/unique_factorization_domain.lean : line 136 : ERR_LIN : Line has more than 100 characters
src/ring_theory/unique_factorization_domain.lean : line 313 : ERR_LIN : Line has more than 100 characters
src/ring_theory/unique_factorization_domain.lean : line 355 : ERR_LIN : Line has more than 100 characters
src/ring_theory/unique_factorization_domain.lean : line 706 : ERR_LIN : Line has more than 100 characters
src/ring_theory/unique_factorization_domain.lean : line 728 : ERR_LIN : Line has more than 100 characters
src/ring_theory/witt_vector/witt_polynomial.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/ring_theory/witt_vector/witt_polynomial.lean : line 137 : ERR_LIN : Line has more than 100 characters
src/ring_theory/witt_vector/witt_polynomial.lean : line 232 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 0e976d9

Please sign in to comment.