diff --git a/scripts/copy-mod-doc-exceptions.txt b/scripts/copy-mod-doc-exceptions.txt index 5d39358ed9851..ec9b1664871c8 100644 --- a/scripts/copy-mod-doc-exceptions.txt +++ b/scripts/copy-mod-doc-exceptions.txt @@ -159,10 +159,10 @@ src/analysis/analytic/basic.lean : line 755 : ERR_LIN : Line has more than 100 c src/analysis/analytic/composition.lean : line 161 : ERR_LIN : Line has more than 100 characters src/analysis/analytic/composition.lean : line 204 : ERR_LIN : Line has more than 100 characters src/analysis/analytic/composition.lean : line 242 : ERR_LIN : Line has more than 100 characters +src/analysis/analytic/composition.lean : line 905 : ERR_LIN : Line has more than 100 characters src/analysis/analytic/composition.lean : line 906 : ERR_LIN : Line has more than 100 characters -src/analysis/analytic/composition.lean : line 907 : ERR_LIN : Line has more than 100 characters -src/analysis/analytic/composition.lean : line 910 : ERR_LIN : Line has more than 100 characters -src/analysis/analytic/composition.lean : line 950 : ERR_LIN : Line has more than 100 characters +src/analysis/analytic/composition.lean : line 909 : ERR_LIN : Line has more than 100 characters +src/analysis/analytic/composition.lean : line 949 : ERR_LIN : Line has more than 100 characters src/analysis/calculus/deriv.lean : line 1095 : ERR_LIN : Line has more than 100 characters src/analysis/calculus/deriv.lean : line 308 : ERR_LIN : Line has more than 100 characters src/analysis/calculus/fderiv.lean : line 1865 : ERR_LIN : Line has more than 100 characters @@ -690,9 +690,6 @@ src/data/equiv/mul_add.lean : line 493 : ERR_LIN : Line has more than 100 charac src/data/equiv/mul_add.lean : line 506 : ERR_LIN : Line has more than 100 characters src/data/equiv/nat.lean : line 12 : ERR_MOD : Module docstring missing, or too late src/data/erased.lean : line 8 : ERR_MOD : Module docstring missing, or too late -src/data/fin.lean : line 1072 : ERR_LIN : Line has more than 100 characters -src/data/fin.lean : line 290 : ERR_LIN : Line has more than 100 characters -src/data/fin.lean : line 386 : ERR_LIN : Line has more than 100 characters src/data/fin2.lean : line 7 : ERR_MOD : Module docstring missing, or too late src/data/finset/gcd.lean : line 133 : ERR_LIN : Line has more than 100 characters src/data/finsupp/pointwise.lean : line 57 : ERR_LIN : Line has more than 100 characters @@ -922,7 +919,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 2302 : ERR_LIN : Line has more than 100 characters +src/data/set/basic.lean : line 2311 : ERR_LIN : Line has more than 100 characters src/data/set/basic.lean : line 469 : ERR_LIN : Line has more than 100 characters src/data/set/basic.lean : line 554 : ERR_LIN : Line has more than 100 characters src/data/set/basic.lean : line 658 : ERR_LIN : Line has more than 100 characters @@ -978,7 +975,7 @@ src/deprecated/subgroup.lean : line 675 : ERR_LIN : Line has more than 100 chara src/deprecated/subring.lean : line 133 : ERR_LIN : Line has more than 100 characters src/deprecated/subring.lean : line 15 : ERR_LIN : Line has more than 100 characters src/deprecated/subring.lean : line 9 : ERR_MOD : Module docstring missing, or too late -src/dynamics/circle/rotation_number/translation_number.lean : line 156 : ERR_LIN : Line has more than 100 characters +src/dynamics/circle/rotation_number/translation_number.lean : line 264 : ERR_LIN : Line has more than 100 characters src/field_theory/algebraic_closure.lean : line 239 : ERR_LIN : Line has more than 100 characters src/field_theory/algebraic_closure.lean : line 66 : ERR_LIN : Line has more than 100 characters src/field_theory/algebraic_closure.lean : line 91 : ERR_LIN : Line has more than 100 characters @@ -1171,9 +1168,9 @@ src/linear_algebra/multilinear.lean : line 509 : ERR_LIN : Line has more than 10 src/linear_algebra/multilinear.lean : line 63 : ERR_LIN : Line has more than 100 characters src/linear_algebra/multilinear.lean : line 78 : ERR_LIN : Line has more than 100 characters src/linear_algebra/special_linear_group.lean : line 53 : ERR_LIN : Line has more than 100 characters -src/logic/basic.lean : line 491 : ERR_LIN : Line has more than 100 characters -src/logic/basic.lean : line 568 : ERR_LIN : Line has more than 100 characters -src/logic/basic.lean : line 868 : ERR_LIN : Line has more than 100 characters +src/logic/basic.lean : line 494 : ERR_LIN : Line has more than 100 characters +src/logic/basic.lean : line 571 : ERR_LIN : Line has more than 100 characters +src/logic/basic.lean : line 871 : ERR_LIN : Line has more than 100 characters src/logic/function/basic.lean : line 322 : ERR_LIN : Line has more than 100 characters src/logic/function/basic.lean : line 496 : ERR_LIN : Line has more than 100 characters src/logic/function/basic.lean : line 536 : ERR_LIN : Line has more than 100 characters @@ -1267,15 +1264,15 @@ src/order/filter/bases.lean : line 259 : ERR_LIN : Line has more than 100 charac src/order/filter/bases.lean : line 40 : ERR_LIN : Line has more than 100 characters src/order/filter/bases.lean : line 625 : ERR_LIN : Line has more than 100 characters src/order/filter/bases.lean : line 86 : ERR_LIN : Line has more than 100 characters -src/order/filter/basic.lean : line 1324 : ERR_LIN : Line has more than 100 characters -src/order/filter/basic.lean : line 1464 : ERR_LIN : Line has more than 100 characters +src/order/filter/basic.lean : line 1327 : ERR_LIN : Line has more than 100 characters +src/order/filter/basic.lean : line 1467 : ERR_LIN : Line has more than 100 characters src/order/filter/basic.lean : line 147 : ERR_LIN : Line has more than 100 characters -src/order/filter/basic.lean : line 1470 : ERR_LIN : Line has more than 100 characters -src/order/filter/basic.lean : line 1487 : ERR_LIN : Line has more than 100 characters -src/order/filter/basic.lean : line 1767 : ERR_LIN : Line has more than 100 characters -src/order/filter/basic.lean : line 1919 : ERR_LIN : Line has more than 100 characters -src/order/filter/basic.lean : line 2047 : ERR_LIN : Line has more than 100 characters -src/order/filter/basic.lean : line 2287 : ERR_LIN : Line has more than 100 characters +src/order/filter/basic.lean : line 1473 : ERR_LIN : Line has more than 100 characters +src/order/filter/basic.lean : line 1490 : ERR_LIN : Line has more than 100 characters +src/order/filter/basic.lean : line 1770 : ERR_LIN : Line has more than 100 characters +src/order/filter/basic.lean : line 1922 : ERR_LIN : Line has more than 100 characters +src/order/filter/basic.lean : line 2050 : ERR_LIN : Line has more than 100 characters +src/order/filter/basic.lean : line 2290 : ERR_LIN : Line has more than 100 characters src/order/filter/basic.lean : line 657 : ERR_LIN : Line has more than 100 characters src/order/filter/basic.lean : line 667 : ERR_LIN : Line has more than 100 characters src/order/filter/extr.lean : line 301 : ERR_LIN : Line has more than 100 characters @@ -1787,7 +1784,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 678 : ERR_LIN : Line has more than 100 characters +src/topology/algebra/infinite_sum.lean : line 697 : 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 @@ -2054,7 +2051,6 @@ src/topology/uniform_space/separation.lean : line 429 : ERR_LIN : Line has more src/topology/uniform_space/separation.lean : line 431 : ERR_LIN : Line has more than 100 characters src/topology/uniform_space/separation.lean : line 46 : ERR_LIN : Line has more than 100 characters src/topology/uniform_space/uniform_convergence.lean : line 320 : ERR_LIN : Line has more than 100 characters -src/topology/uniform_space/uniform_embedding.lean : line 347 : ERR_LIN : Line has more than 100 characters -src/topology/uniform_space/uniform_embedding.lean : line 394 : ERR_LIN : Line has more than 100 characters -src/topology/uniform_space/uniform_embedding.lean : line 401 : ERR_LIN : Line has more than 100 characters -src/topology/uniform_space/uniform_embedding.lean : line 89 : ERR_LIN : Line has more than 100 characters +src/topology/uniform_space/uniform_embedding.lean : line 348 : ERR_LIN : Line has more than 100 characters +src/topology/uniform_space/uniform_embedding.lean : line 395 : ERR_LIN : Line has more than 100 characters +src/topology/uniform_space/uniform_embedding.lean : line 402 : ERR_LIN : Line has more than 100 characters