Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#4665)
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 Oct 18, 2020
1 parent 77dc679 commit c7782bb
Showing 1 changed file with 34 additions and 34 deletions.
68 changes: 34 additions & 34 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -22,10 +22,10 @@ archive/sensitivity.lean : line 411 : ERR_LIN : Line has more than 100 character
archive/sensitivity.lean : line 412 : ERR_LIN : Line has more than 100 characters
archive/sensitivity.lean : line 413 : ERR_LIN : Line has more than 100 characters
archive/sensitivity.lean : line 417 : ERR_LIN : Line has more than 100 characters
src/algebra/algebra/basic.lean : line 1025 : ERR_LIN : Line has more than 100 characters
src/algebra/algebra/basic.lean : line 115 : ERR_LIN : Line has more than 100 characters
src/algebra/algebra/basic.lean : line 720 : ERR_LIN : Line has more than 100 characters
src/algebra/algebra/basic.lean : line 820 : ERR_LIN : Line has more than 100 characters
src/algebra/algebra/basic.lean : line 1042 : ERR_LIN : Line has more than 100 characters
src/algebra/algebra/basic.lean : line 116 : ERR_LIN : Line has more than 100 characters
src/algebra/algebra/basic.lean : line 737 : ERR_LIN : Line has more than 100 characters
src/algebra/algebra/basic.lean : line 837 : ERR_LIN : Line has more than 100 characters
src/algebra/algebra/operations.lean : line 190 : ERR_LIN : Line has more than 100 characters
src/algebra/algebra/operations.lean : line 20 : ERR_LIN : Line has more than 100 characters
src/algebra/algebra/operations.lean : line 99 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -133,27 +133,27 @@ src/algebra/free_algebra.lean : line 264 : ERR_LIN : Line has more than 100 char
src/algebra/free_algebra.lean : line 301 : ERR_LIN : Line has more than 100 characters
src/algebra/free_algebra.lean : line 35 : 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/gcd_monoid.lean : line 159 : ERR_LIN : Line has more than 100 characters
src/algebra/gcd_monoid.lean : line 162 : ERR_LIN : Line has more than 100 characters
src/algebra/gcd_monoid.lean : line 219 : ERR_LIN : Line has more than 100 characters
src/algebra/gcd_monoid.lean : line 256 : ERR_LIN : Line has more than 100 characters
src/algebra/gcd_monoid.lean : line 274 : ERR_LIN : Line has more than 100 characters
src/algebra/gcd_monoid.lean : line 493 : ERR_LIN : Line has more than 100 characters
src/algebra/gcd_monoid.lean : line 175 : ERR_LIN : Line has more than 100 characters
src/algebra/gcd_monoid.lean : line 178 : ERR_LIN : Line has more than 100 characters
src/algebra/gcd_monoid.lean : line 235 : ERR_LIN : Line has more than 100 characters
src/algebra/gcd_monoid.lean : line 272 : ERR_LIN : Line has more than 100 characters
src/algebra/gcd_monoid.lean : line 290 : ERR_LIN : Line has more than 100 characters
src/algebra/gcd_monoid.lean : line 509 : ERR_LIN : Line has more than 100 characters
src/algebra/gcd_monoid.lean : line 52 : ERR_LIN : Line has more than 100 characters
src/algebra/gcd_monoid.lean : line 525 : ERR_LIN : Line has more than 100 characters
src/algebra/gcd_monoid.lean : line 97 : 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/geom_sum.lean : line 182 : ERR_LIN : Line has more than 100 characters
src/algebra/geom_sum.lean : line 34 : ERR_LIN : Line has more than 100 characters
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
src/algebra/group/prod.lean : line 237 : ERR_LIN : Line has more than 100 characters
src/algebra/group/prod.lean : line 238 : ERR_LIN : Line has more than 100 characters
src/algebra/group/prod.lean : line 251 : ERR_LIN : Line has more than 100 characters
src/algebra/group/prod.lean : line 252 : ERR_LIN : Line has more than 100 characters
src/algebra/group/with_one.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/algebra/group_action_hom.lean : line 276 : ERR_LIN : Line has more than 100 characters
src/algebra/group_action_hom.lean : line 287 : ERR_LIN : Line has more than 100 characters
src/algebra/group_power/basic.lean : line 414 : ERR_LIN : Line has more than 100 characters
src/algebra/group_power/basic.lean : line 492 : ERR_LIN : Line has more than 100 characters
src/algebra/group_power/basic.lean : line 501 : ERR_LIN : Line has more than 100 characters
src/algebra/group_power/lemmas.lean : line 475 : ERR_LIN : Line has more than 100 characters
src/algebra/group_ring_action.lean : line 223 : ERR_LIN : Line has more than 100 characters
src/algebra/group_ring_action.lean : line 224 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -198,16 +198,16 @@ src/algebra/monoid_algebra.lean : line 367 : ERR_LIN : Line has more than 100 ch
src/algebra/monoid_algebra.lean : line 386 : ERR_LIN : Line has more than 100 characters
src/algebra/monoid_algebra.lean : line 690 : ERR_LIN : Line has more than 100 characters
src/algebra/monoid_algebra.lean : line 699 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_group.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/algebra/ordered_group.lean : line 1217 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_group.lean : line 1219 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_group.lean : line 1611 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_group.lean : line 621 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_ring.lean : line 1034 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_ring.lean : line 689 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_ring.lean : line 693 : 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 1234 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_group.lean : line 1236 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_group.lean : line 1628 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_group.lean : line 622 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_ring.lean : line 1053 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_ring.lean : line 708 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_ring.lean : line 712 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_ring.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/algebra/ordered_ring.lean : line 803 : ERR_LIN : Line has more than 100 characters
src/algebra/ordered_ring.lean : line 822 : ERR_LIN : Line has more than 100 characters
src/algebra/polynomial/big_operators.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/algebra/punit_instances.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/algebra/quandle.lean : line 461 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -802,7 +802,7 @@ src/data/fin.lean : line 377 : ERR_LIN : Line has more than 100 characters
src/data/fin.lean : line 508 : ERR_LIN : Line has more than 100 characters
src/data/fin2.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/data/finset/gcd.lean : line 133 : ERR_LIN : Line has more than 100 characters
src/data/finsupp/basic.lean : line 1366 : ERR_LIN : Line has more than 100 characters
src/data/finsupp/basic.lean : line 1380 : ERR_LIN : Line has more than 100 characters
src/data/finsupp/basic.lean : line 466 : ERR_LIN : Line has more than 100 characters
src/data/finsupp/pointwise.lean : line 57 : ERR_LIN : Line has more than 100 characters
src/data/fintype/basic.lean : line 15 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -1075,7 +1075,7 @@ src/data/set/finite.lean : line 210 : ERR_LIN : Line has more than 100 character
src/data/set/finite.lean : line 216 : ERR_LIN : Line has more than 100 characters
src/data/set/finite.lean : line 293 : ERR_LIN : Line has more than 100 characters
src/data/set/finite.lean : line 416 : ERR_LIN : Line has more than 100 characters
src/data/set/function.lean : line 401 : ERR_LIN : Line has more than 100 characters
src/data/set/function.lean : line 409 : ERR_LIN : Line has more than 100 characters
src/data/set/lattice.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/data/set/lattice.lean : line 453 : ERR_LIN : Line has more than 100 characters
src/data/set/lattice.lean : line 455 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1122,9 +1122,9 @@ src/deprecated/subring.lean : line 127 : ERR_LIN : Line has more than 100 charac
src/deprecated/subring.lean : line 15 : ERR_LIN : Line has more than 100 characters
src/deprecated/subring.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/dynamics/circle/rotation_number/translation_number.lean : line 156 : ERR_LIN : Line has more than 100 characters
src/field_theory/algebraic_closure.lean : line 238 : ERR_LIN : Line has more than 100 characters
src/field_theory/algebraic_closure.lean : line 65 : ERR_LIN : Line has more than 100 characters
src/field_theory/algebraic_closure.lean : line 90 : ERR_LIN : Line has more than 100 characters
src/field_theory/algebraic_closure.lean : line 239 : ERR_LIN : Line has more than 100 characters
src/field_theory/algebraic_closure.lean : line 66 : ERR_LIN : Line has more than 100 characters
src/field_theory/algebraic_closure.lean : line 91 : ERR_LIN : Line has more than 100 characters
src/field_theory/chevalley_warning.lean : line 144 : ERR_LIN : Line has more than 100 characters
src/field_theory/chevalley_warning.lean : line 80 : ERR_LIN : Line has more than 100 characters
src/field_theory/finite/basic.lean : line 53 : ERR_LIN : Line has more than 100 characters
Expand All @@ -1139,10 +1139,10 @@ src/field_theory/separable.lean : line 222 : ERR_LIN : Line has more than 100 ch
src/field_theory/separable.lean : line 407 : ERR_LIN : Line has more than 100 characters
src/field_theory/separable.lean : line 526 : 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 439 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 488 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 503 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 579 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 440 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 489 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 504 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 580 : 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 @@ -1276,7 +1276,7 @@ src/group_theory/subgroup.lean : line 752 : ERR_LIN : Line has more than 100 cha
src/group_theory/subgroup.lean : line 787 : ERR_LIN : Line has more than 100 characters
src/group_theory/submonoid/operations.lean : line 532 : 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/affine_space/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/linear_algebra/affine_space/basic.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/linear_algebra/affine_space/combination.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/linear_algebra/affine_space/finite_dimensional.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/linear_algebra/affine_space/independent.lean : line 11 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -2243,8 +2243,8 @@ src/topology/sheaves/presheaf.lean : line 58 : ERR_LIN : Line has more than 100
src/topology/sheaves/presheaf.lean : line 94 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/presheaf.lean : line 97 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/presheaf_of_functions.lean : line 80 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf.lean : line 73 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf.lean : line 75 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf.lean : line 89 : ERR_LIN : Line has more than 100 characters
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
Expand Down

0 comments on commit c7782bb

Please sign in to comment.