Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#13637)
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 Apr 23, 2022
1 parent 9923362 commit 79ea30c
Showing 1 changed file with 0 additions and 27 deletions.
27 changes: 0 additions & 27 deletions scripts/nolints.txt
Expand Up @@ -519,33 +519,6 @@ apply_nolint relator.lift_fun doc_blame
apply_nolint relator.right_total doc_blame
apply_nolint relator.right_unique doc_blame

-- measure_theory/constructions/pi.lean
apply_nolint measure_theory.pi.is_inv_invariant_volume to_additive_doc
apply_nolint measure_theory.pi.is_mul_left_invariant_volume to_additive_doc

-- measure_theory/group/integration.lean
apply_nolint measure_theory.integral_eq_zero_of_mul_left_eq_neg to_additive_doc
apply_nolint measure_theory.integral_eq_zero_of_mul_right_eq_neg to_additive_doc
apply_nolint measure_theory.integral_mul_left_eq_self to_additive_doc
apply_nolint measure_theory.integral_mul_right_eq_self to_additive_doc
apply_nolint measure_theory.lintegral_eq_zero_of_is_mul_left_invariant to_additive_doc
apply_nolint measure_theory.lintegral_mul_left_eq_self to_additive_doc
apply_nolint measure_theory.lintegral_mul_right_eq_self to_additive_doc

-- measure_theory/group/measure.lean
apply_nolint measure_theory.forall_measure_preimage_mul_iff to_additive_doc
apply_nolint measure_theory.forall_measure_preimage_mul_right_iff to_additive_doc
apply_nolint measure_theory.is_mul_left_invariant.is_mul_right_invariant to_additive_doc
apply_nolint measure_theory.is_open_pos_measure_of_mul_left_invariant_of_compact to_additive_doc
apply_nolint measure_theory.is_open_pos_measure_of_mul_left_invariant_of_regular to_additive_doc
apply_nolint measure_theory.measure.is_haar_measure.has_no_atoms to_additive_doc
apply_nolint measure_theory.measure.is_haar_measure.sigma_finite to_additive_doc
apply_nolint measure_theory.measure.is_haar_measure_map to_additive_doc
apply_nolint measure_theory.measure.is_haar_measure_of_is_compact_nonempty_interior to_additive_doc
apply_nolint measure_theory.measure_lt_top_of_is_compact_of_is_mul_left_invariant to_additive_doc
apply_nolint measure_theory.measure_lt_top_of_is_compact_of_is_mul_left_invariant' to_additive_doc
apply_nolint measure_theory.measure_preimage_mul to_additive_doc

-- measure_theory/group/prod.lean
apply_nolint measure_theory.absolutely_continuous_of_is_mul_left_invariant to_additive_doc
apply_nolint measure_theory.map_prod_inv_mul_eq to_additive_doc
Expand Down

0 comments on commit 79ea30c

Please sign in to comment.