Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5041)
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 19, 2020
1 parent 68adaba commit 87a6d95
Showing 1 changed file with 30 additions and 28 deletions.
58 changes: 30 additions & 28 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -87,10 +87,10 @@ src/algebra/divisibility.lean : line 230 : ERR_LIN : Line has more than 100 char
src/algebra/euclidean_domain.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/algebra/field.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/algebra/field_power.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/algebra/free_algebra.lean : line 276 : ERR_LIN : Line has more than 100 characters
src/algebra/free_algebra.lean : line 278 : ERR_LIN : Line has more than 100 characters
src/algebra/free_algebra.lean : line 319 : 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_algebra.lean : line 277 : ERR_LIN : Line has more than 100 characters
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/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
Expand Down Expand Up @@ -227,13 +227,13 @@ src/analysis/normed_space/hahn_banach.lean : line 115 : ERR_LIN : Line has more
src/analysis/normed_space/inner_product.lean : line 1033 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1070 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1076 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1195 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1197 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1199 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1207 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1231 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1237 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1238 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1304 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1205 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1229 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1235 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1236 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1302 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 352 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 811 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 830 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -368,9 +368,9 @@ src/category_theory/graded_object.lean : line 70 : ERR_LIN : Line has more than
src/category_theory/graded_object.lean : line 95 : ERR_LIN : Line has more than 100 characters
src/category_theory/groupoid.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/category_theory/hom_functor.lean : line 21 : ERR_LIN : Line has more than 100 characters
src/category_theory/is_connected.lean : line 123 : ERR_LIN : Line has more than 100 characters
src/category_theory/is_connected.lean : line 150 : ERR_LIN : Line has more than 100 characters
src/category_theory/is_connected.lean : line 197 : ERR_LIN : Line has more than 100 characters
src/category_theory/is_connected.lean : line 124 : ERR_LIN : Line has more than 100 characters
src/category_theory/is_connected.lean : line 151 : ERR_LIN : Line has more than 100 characters
src/category_theory/is_connected.lean : line 250 : ERR_LIN : Line has more than 100 characters
src/category_theory/isomorphism.lean : line 112 : ERR_LIN : Line has more than 100 characters
src/category_theory/isomorphism.lean : line 236 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/cofinal.lean : line 184 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -687,13 +687,12 @@ src/data/complex/exponential.lean : line 1189 : ERR_LIN : Line has more than 100
src/data/complex/exponential.lean : line 165 : ERR_LIN : Line has more than 100 characters
src/data/complex/exponential.lean : line 548 : ERR_LIN : Line has more than 100 characters
src/data/complex/exponential.lean : line 841 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 27 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 545 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 550 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 30 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 543 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 548 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 560 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 562 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 564 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 576 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 585 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 584 : ERR_LIN : Line has more than 100 characters
src/data/dlist/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/dlist/instances.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/data/equiv/denumerable.lean : line 14 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -744,8 +743,8 @@ src/data/lazy_list/basic.lean : line 187 : ERR_LIN : Line has more than 100 char
src/data/lazy_list/basic.lean : line 199 : ERR_LIN : Line has more than 100 characters
src/data/lazy_list/basic.lean : line 201 : ERR_LIN : Line has more than 100 characters
src/data/list/bag_inter.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/list/basic.lean : line 1626 : ERR_LIN : Line has more than 100 characters
src/data/list/basic.lean : line 1634 : ERR_LIN : Line has more than 100 characters
src/data/list/basic.lean : line 1642 : ERR_LIN : Line has more than 100 characters
src/data/list/basic.lean : line 1650 : ERR_LIN : Line has more than 100 characters
src/data/list/chain.lean : line 255 : ERR_LIN : Line has more than 100 characters
src/data/list/chain.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/list/erase_dup.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -1433,8 +1432,8 @@ src/ring_theory/localization.lean : line 1315 : ERR_LIN : Line has more than 100
src/ring_theory/localization.lean : line 869 : ERR_LIN : Line has more than 100 characters
src/ring_theory/multiplicity.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/ring_theory/multiplicity.lean : line 142 : 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/multiplicity.lean : line 315 : ERR_LIN : Line has more than 100 characters
src/ring_theory/multiplicity.lean : line 321 : ERR_LIN : Line has more than 100 characters
src/ring_theory/multiplicity.lean : line 322 : 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
Expand Down Expand Up @@ -1805,6 +1804,7 @@ src/topology/algebra/floor_ring.lean : line 12 : ERR_MOD : Module docstring miss
src/topology/algebra/floor_ring.lean : line 183 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/floor_ring.lean : line 187 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 431 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 441 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 460 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group_completion.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/group_completion.lean : line 53 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1867,10 +1867,12 @@ src/topology/category/Top/limits.lean : line 10 : ERR_MOD : Module docstring mis
src/topology/category/Top/limits.lean : line 30 : ERR_LIN : Line has more than 100 characters
src/topology/category/Top/limits.lean : line 32 : ERR_LIN : Line has more than 100 characters
src/topology/category/Top/limits.lean : line 33 : ERR_LIN : Line has more than 100 characters
src/topology/category/Top/limits.lean : line 43 : ERR_LIN : Line has more than 100 characters
src/topology/category/Top/limits.lean : line 61 : ERR_LIN : Line has more than 100 characters
src/topology/category/Top/limits.lean : line 63 : ERR_LIN : Line has more than 100 characters
src/topology/category/Top/limits.lean : line 64 : ERR_LIN : Line has more than 100 characters
src/topology/category/Top/limits.lean : line 72 : ERR_LIN : Line has more than 100 characters
src/topology/category/Top/limits.lean : line 74 : ERR_LIN : Line has more than 100 characters
src/topology/category/Top/limits.lean : line 78 : ERR_LIN : Line has more than 100 characters
src/topology/category/Top/open_nhds.lean : line 45 : ERR_LIN : Line has more than 100 characters
src/topology/category/Top/open_nhds.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Expand All @@ -1885,10 +1887,10 @@ src/topology/dense_embedding.lean : line 231 : ERR_LIN : Line has more than 100
src/topology/dense_embedding.lean : line 276 : ERR_LIN : Line has more than 100 characters
src/topology/dense_embedding.lean : line 294 : ERR_LIN : Line has more than 100 characters
src/topology/dense_embedding.lean : line 97 : ERR_LIN : Line has more than 100 characters
src/topology/homeomorph.lean : line 176 : ERR_LIN : Line has more than 100 characters
src/topology/homeomorph.lean : line 184 : ERR_LIN : Line has more than 100 characters
src/topology/homeomorph.lean : line 178 : ERR_LIN : Line has more than 100 characters
src/topology/homeomorph.lean : line 183 : ERR_LIN : Line has more than 100 characters
src/topology/homeomorph.lean : line 193 : ERR_LIN : Line has more than 100 characters
src/topology/homeomorph.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/topology/homeomorph.lean : line 85 : ERR_LIN : Line has more than 100 characters
src/topology/instances/complex.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/topology/instances/nnreal.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/topology/instances/real.lean : line 128 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1999,8 +2001,8 @@ src/topology/metric_space/lipschitz.lean : line 74 : ERR_LIN : Line has more tha
src/topology/metric_space/premetric_space.lean : line 82 : ERR_LIN : Line has more than 100 characters
src/topology/omega_complete_partial_order.lean : line 85 : ERR_LIN : Line has more than 100 characters
src/topology/opens.lean : line 149 : ERR_LIN : Line has more than 100 characters
src/topology/order.lean : line 284 : ERR_LIN : Line has more than 100 characters
src/topology/order.lean : line 393 : ERR_LIN : Line has more than 100 characters
src/topology/order.lean : line 288 : ERR_LIN : Line has more than 100 characters
src/topology/order.lean : line 401 : ERR_LIN : Line has more than 100 characters
src/topology/order.lean : line 96 : ERR_LIN : Line has more than 100 characters
src/topology/path_connected.lean : line 298 : ERR_LIN : Line has more than 100 characters
src/topology/path_connected.lean : line 497 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 87a6d95

Please sign in to comment.