diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt index eae2f07d7b46a..027ca58b927e8 100644 --- a/scripts/style-exceptions.txt +++ b/scripts/style-exceptions.txt @@ -685,8 +685,8 @@ src/data/set/disjointed.lean : line 10 : ERR_MOD : Module docstring missing, or src/data/set/enumerate.lean : line 10 : ERR_MOD : Module docstring missing, or too late src/data/set/function.lean : line 420 : ERR_LIN : Line has more than 100 characters src/data/set/lattice.lean : line 13 : ERR_MOD : Module docstring missing, or too late -src/data/set/lattice.lean : line 466 : ERR_LIN : Line has more than 100 characters -src/data/set/lattice.lean : line 468 : ERR_LIN : Line has more than 100 characters +src/data/set/lattice.lean : line 470 : ERR_LIN : Line has more than 100 characters +src/data/set/lattice.lean : line 472 : ERR_LIN : Line has more than 100 characters src/data/setoid/basic.lean : line 252 : ERR_LIN : Line has more than 100 characters src/data/sigma/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late src/data/string/basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late @@ -763,12 +763,12 @@ src/geometry/manifold/basic_smooth_bundle.lean : line 391 : ERR_LIN : Line has m src/geometry/manifold/basic_smooth_bundle.lean : line 41 : ERR_LIN : Line has more than 100 characters src/geometry/manifold/basic_smooth_bundle.lean : line 421 : ERR_LIN : Line has more than 100 characters src/geometry/manifold/basic_smooth_bundle.lean : line 563 : ERR_LIN : Line has more than 100 characters -src/geometry/manifold/charted_space.lean : line 488 : ERR_LIN : Line has more than 100 characters -src/geometry/manifold/charted_space.lean : line 490 : ERR_LIN : Line has more than 100 characters -src/geometry/manifold/charted_space.lean : line 493 : ERR_LIN : Line has more than 100 characters -src/geometry/manifold/charted_space.lean : line 541 : ERR_LIN : Line has more than 100 characters -src/geometry/manifold/charted_space.lean : line 813 : ERR_LIN : Line has more than 100 characters -src/geometry/manifold/charted_space.lean : line 858 : ERR_LIN : Line has more than 100 characters +src/geometry/manifold/charted_space.lean : line 494 : ERR_LIN : Line has more than 100 characters +src/geometry/manifold/charted_space.lean : line 496 : ERR_LIN : Line has more than 100 characters +src/geometry/manifold/charted_space.lean : line 499 : ERR_LIN : Line has more than 100 characters +src/geometry/manifold/charted_space.lean : line 547 : ERR_LIN : Line has more than 100 characters +src/geometry/manifold/charted_space.lean : line 819 : ERR_LIN : Line has more than 100 characters +src/geometry/manifold/charted_space.lean : line 864 : ERR_LIN : Line has more than 100 characters src/geometry/manifold/instances/real.lean : line 18 : ERR_LIN : Line has more than 100 characters src/geometry/manifold/instances/real.lean : line 303 : ERR_LIN : Line has more than 100 characters src/geometry/manifold/instances/real.lean : line 79 : ERR_LIN : Line has more than 100 characters @@ -836,26 +836,6 @@ src/group_theory/order_of_element.lean : line 442 : ERR_LIN : Line has more than src/group_theory/order_of_element.lean : line 472 : ERR_LIN : Line has more than 100 characters src/group_theory/order_of_element.lean : line 517 : ERR_LIN : Line has more than 100 characters src/group_theory/order_of_element.lean : line 519 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/cycles.lean : line 257 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/cycles.lean : line 260 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/cycles.lean : line 271 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/cycles.lean : line 30 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/cycles.lean : line 71 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/cycles.lean : line 78 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/cycles.lean : line 8 : ERR_MOD : Module docstring missing, or too late -src/group_theory/perm/cycles.lean : line 81 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/cycles.lean : line 84 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/cycles.lean : line 85 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/cycles.lean : line 86 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/sign.lean : line 117 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/sign.lean : line 124 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/sign.lean : line 127 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/sign.lean : line 130 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/sign.lean : line 160 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/sign.lean : line 257 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/sign.lean : line 286 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/sign.lean : line 468 : ERR_LIN : Line has more than 100 characters -src/group_theory/perm/sign.lean : line 51 : ERR_LIN : Line has more than 100 characters src/group_theory/presented_group.lean : line 11 : ERR_MOD : Module docstring missing, or too late src/group_theory/presented_group.lean : line 51 : ERR_LIN : Line has more than 100 characters src/group_theory/quotient_group.lean : line 10 : ERR_MOD : Module docstring missing, or too late @@ -1546,7 +1526,7 @@ src/topology/metric_space/gromov_hausdorff_realized.lean : line 234 : ERR_LIN : src/topology/metric_space/gromov_hausdorff_realized.lean : line 404 : ERR_LIN : Line has more than 100 characters src/topology/metric_space/gromov_hausdorff_realized.lean : line 75 : ERR_LIN : Line has more than 100 characters src/topology/metric_space/gromov_hausdorff_realized.lean : line 77 : ERR_LIN : Line has more than 100 characters -src/topology/metric_space/isometry.lean : line 319 : ERR_LIN : Line has more than 100 characters +src/topology/metric_space/isometry.lean : line 356 : ERR_LIN : Line has more than 100 characters src/topology/metric_space/lipschitz.lean : line 74 : 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