diff --git a/scripts/copy-mod-doc-exceptions.txt b/scripts/copy-mod-doc-exceptions.txt index 7f4ce9e92a65f..9075f4724c3c5 100644 --- a/scripts/copy-mod-doc-exceptions.txt +++ b/scripts/copy-mod-doc-exceptions.txt @@ -763,10 +763,10 @@ src/data/matrix/pequiv.lean : line 137 : ERR_LIN : Line has more than 100 charac src/data/matrix/pequiv.lean : line 143 : ERR_LIN : Line has more than 100 characters src/data/matrix/pequiv.lean : line 8 : ERR_MOD : Module docstring missing, or too late src/data/mllist.lean : line 14 : ERR_MOD : Module docstring missing, or too late -src/data/multiset/basic.lean : line 1035 : ERR_LIN : Line has more than 100 characters +src/data/multiset/basic.lean : line 1036 : ERR_LIN : Line has more than 100 characters src/data/multiset/basic.lean : line 116 : ERR_LIN : Line has more than 100 characters src/data/multiset/basic.lean : line 128 : ERR_LIN : Line has more than 100 characters -src/data/multiset/basic.lean : line 1289 : ERR_LIN : Line has more than 100 characters +src/data/multiset/basic.lean : line 1290 : ERR_LIN : Line has more than 100 characters src/data/multiset/basic.lean : line 133 : ERR_LIN : Line has more than 100 characters src/data/multiset/basic.lean : line 1727 : ERR_LIN : Line has more than 100 characters src/data/multiset/basic.lean : line 1736 : ERR_LIN : Line has more than 100 characters @@ -774,15 +774,15 @@ src/data/multiset/basic.lean : line 1752 : ERR_LIN : Line has more than 100 char src/data/multiset/basic.lean : line 1755 : ERR_LIN : Line has more than 100 characters src/data/multiset/basic.lean : line 1944 : ERR_LIN : Line has more than 100 characters src/data/multiset/basic.lean : line 2063 : ERR_LIN : Line has more than 100 characters -src/data/multiset/basic.lean : line 542 : ERR_LIN : Line has more than 100 characters -src/data/multiset/basic.lean : line 666 : ERR_LIN : Line has more than 100 characters -src/data/multiset/basic.lean : line 677 : ERR_LIN : Line has more than 100 characters -src/data/multiset/basic.lean : line 684 : ERR_LIN : Line has more than 100 characters -src/data/multiset/basic.lean : line 704 : ERR_LIN : Line has more than 100 characters -src/data/multiset/basic.lean : line 707 : ERR_LIN : Line has more than 100 characters -src/data/multiset/basic.lean : line 719 : ERR_LIN : Line has more than 100 characters -src/data/multiset/basic.lean : line 722 : ERR_LIN : Line has more than 100 characters -src/data/multiset/basic.lean : line 972 : ERR_LIN : Line has more than 100 characters +src/data/multiset/basic.lean : line 543 : ERR_LIN : Line has more than 100 characters +src/data/multiset/basic.lean : line 667 : ERR_LIN : Line has more than 100 characters +src/data/multiset/basic.lean : line 678 : ERR_LIN : Line has more than 100 characters +src/data/multiset/basic.lean : line 685 : ERR_LIN : Line has more than 100 characters +src/data/multiset/basic.lean : line 705 : ERR_LIN : Line has more than 100 characters +src/data/multiset/basic.lean : line 708 : ERR_LIN : Line has more than 100 characters +src/data/multiset/basic.lean : line 720 : ERR_LIN : Line has more than 100 characters +src/data/multiset/basic.lean : line 723 : ERR_LIN : Line has more than 100 characters +src/data/multiset/basic.lean : line 973 : ERR_LIN : Line has more than 100 characters src/data/multiset/fold.lean : line 25 : ERR_LIN : Line has more than 100 characters src/data/multiset/fold.lean : line 32 : ERR_LIN : Line has more than 100 characters src/data/multiset/fold.lean : line 49 : ERR_LIN : Line has more than 100 characters @@ -1130,15 +1130,15 @@ src/group_theory/subgroup.lean : line 803 : ERR_LIN : Line has more than 100 cha src/group_theory/subgroup.lean : line 838 : 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/basic.lean : line 1522 : ERR_LIN : Line has more than 100 characters -src/linear_algebra/basic.lean : line 1554 : ERR_LIN : Line has more than 100 characters -src/linear_algebra/basic.lean : line 1930 : ERR_LIN : Line has more than 100 characters -src/linear_algebra/basic.lean : line 2040 : ERR_LIN : Line has more than 100 characters -src/linear_algebra/basic.lean : line 2046 : ERR_LIN : Line has more than 100 characters -src/linear_algebra/basic.lean : line 2047 : ERR_LIN : Line has more than 100 characters -src/linear_algebra/basic.lean : line 2054 : ERR_LIN : Line has more than 100 characters -src/linear_algebra/basic.lean : line 2112 : ERR_LIN : Line has more than 100 characters -src/linear_algebra/basic.lean : line 2180 : ERR_LIN : Line has more than 100 characters +src/linear_algebra/basic.lean : line 1520 : ERR_LIN : Line has more than 100 characters +src/linear_algebra/basic.lean : line 1552 : ERR_LIN : Line has more than 100 characters +src/linear_algebra/basic.lean : line 1928 : ERR_LIN : Line has more than 100 characters +src/linear_algebra/basic.lean : line 2038 : ERR_LIN : Line has more than 100 characters +src/linear_algebra/basic.lean : line 2044 : ERR_LIN : Line has more than 100 characters +src/linear_algebra/basic.lean : line 2045 : ERR_LIN : Line has more than 100 characters +src/linear_algebra/basic.lean : line 2052 : ERR_LIN : Line has more than 100 characters +src/linear_algebra/basic.lean : line 2110 : ERR_LIN : Line has more than 100 characters +src/linear_algebra/basic.lean : line 2178 : ERR_LIN : Line has more than 100 characters src/linear_algebra/basis.lean : line 93 : ERR_LIN : Line has more than 100 characters src/linear_algebra/char_poly/coeff.lean : line 190 : ERR_LIN : Line has more than 100 characters src/linear_algebra/char_poly/coeff.lean : line 24 : ERR_LIN : Line has more than 100 characters @@ -1787,7 +1787,7 @@ src/topology/algebra/group_completion.lean : line 69 : ERR_LIN : Line has more t src/topology/algebra/group_completion.lean : line 75 : ERR_LIN : Line has more than 100 characters src/topology/algebra/group_completion.lean : line 82 : ERR_LIN : Line has more than 100 characters src/topology/algebra/group_completion.lean : line 84 : ERR_LIN : Line has more than 100 characters -src/topology/algebra/infinite_sum.lean : line 675 : ERR_LIN : Line has more than 100 characters +src/topology/algebra/infinite_sum.lean : line 678 : ERR_LIN : Line has more than 100 characters src/topology/algebra/module.lean : line 1078 : ERR_LIN : Line has more than 100 characters src/topology/algebra/module.lean : line 1088 : ERR_LIN : Line has more than 100 characters src/topology/algebra/module.lean : line 300 : ERR_LIN : Line has more than 100 characters diff --git a/scripts/nolints.txt b/scripts/nolints.txt index 3fbc029012f79..3895731cf8141 100644 --- a/scripts/nolints.txt +++ b/scripts/nolints.txt @@ -317,7 +317,6 @@ apply_nolint tactic.mllist.take doc_blame unused_arguments apply_nolint tactic.mllist.uncons doc_blame unused_arguments -- data/multiset/basic.lean -apply_nolint multiset.choose doc_blame apply_nolint multiset.decidable_exists_multiset doc_blame apply_nolint multiset.decidable_forall_multiset doc_blame apply_nolint multiset.rec_on doc_blame