Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#4961)
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 10, 2020
1 parent e8758ae commit 1ada09b
Showing 1 changed file with 12 additions and 13 deletions.
25 changes: 12 additions & 13 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -947,7 +947,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 2267 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 2270 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 467 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 552 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 656 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1122,7 +1122,7 @@ src/group_theory/free_group.lean : line 18 : ERR_MOD : Module docstring missing,
src/group_theory/free_group.lean : line 180 : ERR_LIN : Line has more than 100 characters
src/group_theory/free_group.lean : line 672 : ERR_LIN : Line has more than 100 characters
src/group_theory/free_group.lean : line 737 : ERR_LIN : Line has more than 100 characters
src/group_theory/group_action.lean : line 387 : ERR_LIN : Line has more than 100 characters
src/group_theory/group_action.lean : line 386 : ERR_LIN : Line has more than 100 characters
src/group_theory/group_action.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/group_theory/order_of_element.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/group_theory/order_of_element.lean : line 373 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1219,7 +1219,7 @@ src/logic/relation.lean : line 10 : ERR_MOD : Module docstring missing, or too l
src/logic/relator.lean : line 9 : 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 1725 : ERR_LIN : Line has more than 100 characters
src/measure_theory/measure_space.lean : line 1721 : 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 @@ -1435,8 +1435,8 @@ src/ring_theory/jacobson_ideal.lean : line 253 : ERR_LIN : Line has more than 10
src/ring_theory/jacobson_ideal.lean : line 66 : ERR_LIN : Line has more than 100 characters
src/ring_theory/jacobson_ideal.lean : line 86 : ERR_LIN : Line has more than 100 characters
src/ring_theory/jacobson_ideal.lean : line 96 : ERR_LIN : Line has more than 100 characters
src/ring_theory/localization.lean : line 1141 : ERR_LIN : Line has more than 100 characters
src/ring_theory/localization.lean : line 1303 : ERR_LIN : Line has more than 100 characters
src/ring_theory/localization.lean : line 1142 : ERR_LIN : Line has more than 100 characters
src/ring_theory/localization.lean : line 1304 : ERR_LIN : Line has more than 100 characters
src/ring_theory/localization.lean : line 864 : 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
Expand Down Expand Up @@ -1830,13 +1830,13 @@ src/topology/algebra/multilinear.lean : line 185 : 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 1272 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 1728 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 1846 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 1867 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 40 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 423 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 427 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 1369 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 1825 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 1943 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 1964 : 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 424 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 428 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/polynomial.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/ring.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/uniform_group.lean : line 102 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -2050,7 +2050,6 @@ src/topology/sheaves/stalks.lean : line 11 : ERR_MOD : Module docstring missing,
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 1099 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 1301 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 569 : 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 745 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 1ada09b

Please sign in to comment.