diff --git a/scripts/nolints.txt b/scripts/nolints.txt index f4e27ad91c306..09b1c33cc2769 100644 --- a/scripts/nolints.txt +++ b/scripts/nolints.txt @@ -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 diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt index 45222b5f3616c..f6abace32d462 100644 --- a/scripts/style-exceptions.txt +++ b/scripts/style-exceptions.txt @@ -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 @@ -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 @@ -544,11 +544,11 @@ 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 @@ -556,7 +556,7 @@ src/topology/local_homeomorph.lean : line 567 : ERR_LIN : Line has more than 100 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