Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5720)
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 committed Jan 13, 2021
1 parent 5a532ca commit b9b6b16
Showing 1 changed file with 6 additions and 20 deletions.
26 changes: 6 additions & 20 deletions scripts/style-exceptions.txt
Expand Up @@ -363,8 +363,6 @@ src/category_theory/limits/limits.lean : line 566 : ERR_LIN : Line has more than
src/category_theory/limits/limits.lean : line 776 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 827 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/opposites.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/over.lean : line 72 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/over.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/pi.lean : line 58 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/pi.lean : line 88 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/preserves/basic.lean : line 101 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -399,17 +397,6 @@ src/category_theory/limits/shapes/biproducts.lean : line 26 : ERR_LIN : Line has
src/category_theory/limits/shapes/biproducts.lean : line 434 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/biproducts.lean : line 631 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/biproducts.lean : line 645 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/constructions/binary_products.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/shapes/constructions/over/connected.lean : line 57 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/constructions/over/default.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/shapes/constructions/over/products.lean : line 106 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/constructions/over/products.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/shapes/constructions/over/products.lean : line 23 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/constructions/over/products.lean : line 25 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/constructions/over/products.lean : line 66 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/constructions/over/products.lean : line 86 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/constructions/over/products.lean : line 87 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/constructions/pullbacks.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/shapes/finite_limits.lean : line 146 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/finite_limits.lean : line 149 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/finite_limits.lean : line 186 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -865,14 +852,14 @@ 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 2411 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 2414 : 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
src/data/set/basic.lean : line 772 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 971 : ERR_LIN : Line has more than 100 characters
src/data/set/countable.lean : line 122 : ERR_LIN : Line has more than 100 characters
src/data/set/countable.lean : line 138 : ERR_LIN : Line has more than 100 characters
src/data/set/countable.lean : line 143 : ERR_LIN : Line has more than 100 characters
src/data/set/countable.lean : line 159 : ERR_LIN : Line has more than 100 characters
src/data/set/disjointed.lean : line 10 : ERR_MOD : Module docstring missing, or too late
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
Expand Down Expand Up @@ -1070,8 +1057,8 @@ src/group_theory/presented_group.lean : line 51 : ERR_LIN : Line has more than 1
src/group_theory/quotient_group.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/group_theory/semidirect_product.lean : line 52 : ERR_LIN : Line has more than 100 characters
src/group_theory/subgroup.lean : line 377 : ERR_LIN : Line has more than 100 characters
src/group_theory/subgroup.lean : line 826 : ERR_LIN : Line has more than 100 characters
src/group_theory/subgroup.lean : line 861 : ERR_LIN : Line has more than 100 characters
src/group_theory/subgroup.lean : line 845 : ERR_LIN : Line has more than 100 characters
src/group_theory/subgroup.lean : line 880 : ERR_LIN : Line has more than 100 characters
src/group_theory/submonoid/operations.lean : line 560 : 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/basis.lean : line 291 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1115,7 +1102,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 1775 : ERR_LIN : Line has more than 100 characters
src/measure_theory/measure_space.lean : line 1798 : 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 @@ -1683,7 +1670,6 @@ src/topology/algebra/group_completion.lean : line 84 : ERR_LIN : Line has more t
src/topology/algebra/group_completion.lean : line 90 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group_completion.lean : line 97 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group_completion.lean : line 99 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/infinite_sum.lean : line 725 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 1080 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 1090 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 300 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit b9b6b16

Please sign in to comment.