Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5699)
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 11, 2021
1 parent 08800bb commit c112ad0
Showing 1 changed file with 24 additions and 25 deletions.
49 changes: 24 additions & 25 deletions scripts/style-exceptions.txt
View file
Expand Up @@ -633,9 +633,9 @@ src/data/equiv/local_equiv.lean : line 316 : ERR_LIN : Line has more than 100 ch
src/data/equiv/local_equiv.lean : line 333 : ERR_LIN : Line has more than 100 characters
src/data/equiv/local_equiv.lean : line 370 : ERR_LIN : Line has more than 100 characters
src/data/equiv/local_equiv.lean : line 580 : ERR_LIN : Line has more than 100 characters
src/data/equiv/mul_add.lean : line 382 : ERR_LIN : Line has more than 100 characters
src/data/equiv/mul_add.lean : line 398 : ERR_LIN : Line has more than 100 characters
src/data/equiv/mul_add.lean : line 411 : ERR_LIN : Line has more than 100 characters
src/data/equiv/mul_add.lean : line 394 : ERR_LIN : Line has more than 100 characters
src/data/equiv/mul_add.lean : line 410 : ERR_LIN : Line has more than 100 characters
src/data/equiv/mul_add.lean : line 423 : ERR_LIN : Line has more than 100 characters
src/data/equiv/nat.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/data/erased.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/fin2.lean : line 7 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -865,7 +865,7 @@ 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 2396 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 2411 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 474 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 559 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 668 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1115,7 +1115,7 @@ src/logic/relation.lean : line 10 : ERR_MOD : Module docstring missing, or too l
src/logic/relator.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/measure_theory/category/Meas.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/measure_theory/decomposition.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/measure_theory/measure_space.lean : line 1760 : ERR_LIN : Line has more than 100 characters
src/measure_theory/measure_space.lean : line 1775 : ERR_LIN : Line has more than 100 characters
src/measure_theory/measure_space.lean : line 65 : ERR_LIN : Line has more than 100 characters
src/meta/coinductive_predicates.lean : line 115 : ERR_LIN : Line has more than 100 characters
src/meta/coinductive_predicates.lean : line 12 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1201,17 +1201,16 @@ src/order/filter/bases.lean : line 259 : ERR_LIN : Line has more than 100 charac
src/order/filter/bases.lean : line 40 : ERR_LIN : Line has more than 100 characters
src/order/filter/bases.lean : line 625 : ERR_LIN : Line has more than 100 characters
src/order/filter/bases.lean : line 86 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1334 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 147 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1474 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1480 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1497 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1783 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1935 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2063 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2308 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 669 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 679 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1377 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1517 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1523 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1540 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1826 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1978 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2106 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2351 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 675 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 685 : 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 150 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1676,9 +1675,9 @@ src/topology/algebra/continuous_functions.lean : line 87 : ERR_LIN : Line has mo
src/topology/algebra/floor_ring.lean : line 12 : ERR_MOD : Module docstring missing, or too late
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 509 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 519 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 538 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 527 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 537 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 556 : 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 84 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group_completion.lean : line 90 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1909,12 +1908,12 @@ src/topology/sheaves/sheaf_of_functions.lean : line 168 : ERR_LIN : Line has mor
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
src/topology/sheaves/stalks.lean : line 133 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 1123 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 1295 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 1384 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 663 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 69 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 769 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 1163 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 1335 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 1424 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 32 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 703 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 809 : ERR_LIN : Line has more than 100 characters
src/topology/tactic.lean : line 84 : ERR_LIN : Line has more than 100 characters
src/topology/topological_fiber_bundle.lean : line 135 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/absolute_value.lean : line 71 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit c112ad0

Please sign in to comment.