Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#4341)
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 Oct 1, 2020
1 parent bcc7c02 commit af99416
Showing 1 changed file with 0 additions and 16 deletions.
16 changes: 0 additions & 16 deletions scripts/nolints.txt
Expand Up @@ -127,22 +127,6 @@ apply_nolint category_theory.monoidal_functor has_inhabited_instance
apply_nolint category_theory.monoidal_functor.ε_iso doc_blame
apply_nolint category_theory.monoidal_functor.μ_iso doc_blame

-- category_theory/opposites.lean
apply_nolint category_theory.functor.left_op doc_blame
apply_nolint category_theory.functor.op doc_blame
apply_nolint category_theory.functor.op_hom doc_blame
apply_nolint category_theory.functor.op_inv doc_blame
apply_nolint category_theory.functor.right_op doc_blame
apply_nolint category_theory.functor.unop doc_blame
apply_nolint category_theory.has_hom.hom.op doc_blame
apply_nolint category_theory.has_hom.hom.unop doc_blame
apply_nolint category_theory.is_iso_of_op doc_blame
apply_nolint category_theory.iso.op doc_blame
apply_nolint category_theory.nat_trans.left_op doc_blame
apply_nolint category_theory.nat_trans.op doc_blame
apply_nolint category_theory.nat_trans.right_op doc_blame
apply_nolint category_theory.nat_trans.unop doc_blame

-- category_theory/products/basic.lean
apply_nolint category_theory.evaluation doc_blame
apply_nolint category_theory.evaluation_uncurried doc_blame
Expand Down

0 comments on commit af99416

Please sign in to comment.