Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5682)
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 10, 2021
1 parent f60c184 commit a28602a
Showing 1 changed file with 24 additions and 22 deletions.
46 changes: 24 additions & 22 deletions scripts/style-exceptions.txt
View file
Expand Up @@ -93,8 +93,8 @@ 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 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 1103 : ERR_LIN : Line has more than 100 characters
src/algebra/lie/basic.lean : line 1284 : 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
Expand Down Expand Up @@ -436,11 +436,11 @@ src/category_theory/limits/shapes/products.lean : line 56 : ERR_LIN : Line has m
src/category_theory/limits/shapes/products.lean : line 59 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/products.lean : line 60 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/products.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/shapes/pullbacks.lean : line 177 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/pullbacks.lean : line 238 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/pullbacks.lean : line 270 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/pullbacks.lean : line 308 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/pullbacks.lean : line 369 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/pullbacks.lean : line 179 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/pullbacks.lean : line 240 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/pullbacks.lean : line 272 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/pullbacks.lean : line 310 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/pullbacks.lean : line 371 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/pullbacks.lean : line 97 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/regular_mono.lean : line 110 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/regular_mono.lean : line 139 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -877,8 +877,8 @@ src/data/set/disjointed.lean : line 10 : ERR_MOD : Module docstring missing, or
src/data/set/enumerate.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/data/set/function.lean : line 420 : 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
src/data/set/lattice.lean : line 466 : ERR_LIN : Line has more than 100 characters
src/data/set/lattice.lean : line 468 : ERR_LIN : Line has more than 100 characters
src/data/setoid/basic.lean : line 252 : ERR_LIN : Line has more than 100 characters
src/data/sigma/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/string/basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -1214,10 +1214,10 @@ src/order/filter/basic.lean : line 669 : ERR_LIN : Line has more than 100 charac
src/order/filter/basic.lean : line 679 : ERR_LIN : Line has more than 100 characters
src/order/filter/extr.lean : line 301 : ERR_LIN : Line has more than 100 characters
src/order/filter/extr.lean : line 66 : ERR_LIN : Line has more than 100 characters
src/order/filter/lift.lean : line 146 : ERR_LIN : Line has more than 100 characters
src/order/filter/lift.lean : line 247 : ERR_LIN : Line has more than 100 characters
src/order/filter/lift.lean : line 262 : ERR_LIN : Line has more than 100 characters
src/order/filter/lift.lean : line 328 : ERR_LIN : Line has more than 100 characters
src/order/filter/lift.lean : line 150 : ERR_LIN : Line has more than 100 characters
src/order/filter/lift.lean : line 255 : ERR_LIN : Line has more than 100 characters
src/order/filter/lift.lean : line 270 : ERR_LIN : Line has more than 100 characters
src/order/filter/lift.lean : line 336 : ERR_LIN : Line has more than 100 characters
src/order/filter/partial.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/order/fixed_points.lean : line 203 : ERR_LIN : Line has more than 100 characters
src/order/fixed_points.lean : line 207 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1697,7 +1697,7 @@ src/topology/algebra/multilinear.lean : line 245 : ERR_LIN : Line has more than
src/topology/algebra/multilinear.lean : line 46 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/multilinear.lean : line 60 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/open_subgroup.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/ordered.lean : line 1766 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 1782 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 41 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 430 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 434 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1766,13 +1766,13 @@ src/topology/local_extr.lean : line 267 : ERR_LIN : Line has more than 100 chara
src/topology/local_homeomorph.lean : line 503 : ERR_LIN : Line has more than 100 characters
src/topology/local_homeomorph.lean : line 514 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 109 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 1309 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 1321 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 15 : ERR_MOD : Module docstring missing, or too late
src/topology/metric_space/basic.lean : line 1672 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 1684 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 332 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 450 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 776 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 803 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 788 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 815 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/closeds.lean : line 12 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/closeds.lean : line 138 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/closeds.lean : line 188 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1874,10 +1874,12 @@ src/topology/path_connected.lean : line 583 : ERR_LIN : Line has more than 100 c
src/topology/path_connected.lean : line 591 : ERR_LIN : Line has more than 100 characters
src/topology/path_connected.lean : line 655 : ERR_LIN : Line has more than 100 characters
src/topology/separation.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/topology/separation.lean : line 450 : ERR_LIN : Line has more than 100 characters
src/topology/separation.lean : line 516 : ERR_LIN : Line has more than 100 characters
src/topology/separation.lean : line 603 : ERR_LIN : Line has more than 100 characters
src/topology/separation.lean : line 606 : ERR_LIN : Line has more than 100 characters
src/topology/separation.lean : line 167 : ERR_LIN : Line has more than 100 characters
src/topology/separation.lean : line 178 : ERR_LIN : Line has more than 100 characters
src/topology/separation.lean : line 489 : ERR_LIN : Line has more than 100 characters
src/topology/separation.lean : line 555 : ERR_LIN : Line has more than 100 characters
src/topology/separation.lean : line 642 : ERR_LIN : Line has more than 100 characters
src/topology/separation.lean : line 645 : ERR_LIN : Line has more than 100 characters
src/topology/sequences.lean : line 183 : ERR_LIN : Line has more than 100 characters
src/topology/sequences.lean : line 210 : ERR_LIN : Line has more than 100 characters
src/topology/sequences.lean : line 274 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit a28602a

Please sign in to comment.