Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#6686)
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 Mar 15, 2021
1 parent 0a16148 commit c5796c7
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 18 deletions.
13 changes: 0 additions & 13 deletions scripts/nolints.txt
Expand Up @@ -392,19 +392,6 @@ apply_nolint polynomial.eval_sub_factor doc_blame
apply_nolint polynomial.pow_add_expansion doc_blame
apply_nolint polynomial.pow_sub_pow_factor doc_blame

-- data/rat/basic.lean
apply_nolint rat.add doc_blame
apply_nolint rat.inv doc_blame
apply_nolint rat.mul doc_blame
apply_nolint rat.neg doc_blame
apply_nolint rat.num_denom_cases_on doc_blame
apply_nolint rat.num_denom_cases_on' doc_blame
apply_nolint rat.repr doc_blame

-- data/rat/order.lean
apply_nolint rat.le doc_blame
apply_nolint rat.nonneg doc_blame

-- data/real/cau_seq_completion.lean
apply_nolint cau_seq.completion.Cauchy doc_blame
apply_nolint cau_seq.completion.field doc_blame
Expand Down
10 changes: 5 additions & 5 deletions scripts/style-exceptions.txt
Expand Up @@ -99,7 +99,7 @@ src/data/matrix/pequiv.lean : line 8 : ERR_MOD : Module docstring missing, or to
src/data/mllist.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/data/multiset/range.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/mv_polynomial/variables.lean : line 628 : ERR_LIN : Line has more than 100 characters
src/data/nat/basic.lean : line 886 : ERR_LIN : Line has more than 100 characters
src/data/nat/basic.lean : line 901 : ERR_LIN : Line has more than 100 characters
src/data/nat/cast.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/nat/dist.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/data/nat/gcd.lean : line 200 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -164,7 +164,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 2431 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 2435 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 897 : 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
Expand Down Expand Up @@ -544,19 +544,19 @@ src/testing/slim_check/testable.lean : line 741 : ERR_LIN : Line has more than 1
src/topology/algebra/floor_ring.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/group_completion.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/open_subgroup.lean : line 10 : 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/ring.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/uniform_ring.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/uniform_ring.lean : line 148 : ERR_LIN : Line has more than 100 characters
src/topology/bases.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/topology/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/topology/basic.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/topology/category/Top/open_nhds.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/topology/homeomorph.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/topology/instances/real.lean : line 136 : ERR_LIN : Line has more than 100 characters
src/topology/local_homeomorph.lean : line 567 : ERR_LIN : Line has more than 100 characters
src/topology/local_homeomorph.lean : line 578 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 17 : ERR_MOD : Module docstring missing, or too late
src/topology/metric_space/gromov_hausdorff.lean : line 61 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/isometry.lean : line 381 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/isometry.lean : line 385 : ERR_LIN : Line has more than 100 characters
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/separation.lean : line 11 : ERR_MOD : Module docstring missing, or too late
Expand Down

0 comments on commit c5796c7

Please sign in to comment.