Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#2395)
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 12, 2020
1 parent ee8cb15 commit 0f89392
Showing 1 changed file with 0 additions and 25 deletions.
25 changes: 0 additions & 25 deletions scripts/nolints.txt
Original file line number Diff line number Diff line change
Expand Up @@ -390,31 +390,6 @@ apply_nolint category_theory.mono doc_blame
apply_nolint category_theory.obviously' doc_blame
apply_nolint obviously.attr doc_blame

-- category_theory/comma.lean
apply_nolint category_theory.comma doc_blame has_inhabited_instance
apply_nolint category_theory.comma.fst doc_blame
apply_nolint category_theory.comma.map_left doc_blame
apply_nolint category_theory.comma.map_left_comp doc_blame
apply_nolint category_theory.comma.map_left_id doc_blame
apply_nolint category_theory.comma.map_right doc_blame
apply_nolint category_theory.comma.map_right_comp doc_blame
apply_nolint category_theory.comma.map_right_id doc_blame
apply_nolint category_theory.comma.nat_trans doc_blame
apply_nolint category_theory.comma.snd doc_blame
apply_nolint category_theory.comma_morphism doc_blame has_inhabited_instance
apply_nolint category_theory.over doc_blame has_inhabited_instance
apply_nolint category_theory.over.forget doc_blame
apply_nolint category_theory.over.hom_mk doc_blame
apply_nolint category_theory.over.map doc_blame
apply_nolint category_theory.over.mk doc_blame
apply_nolint category_theory.over.post doc_blame
apply_nolint category_theory.under doc_blame has_inhabited_instance
apply_nolint category_theory.under.forget doc_blame
apply_nolint category_theory.under.hom_mk doc_blame
apply_nolint category_theory.under.map doc_blame
apply_nolint category_theory.under.mk doc_blame
apply_nolint category_theory.under.post doc_blame

-- category_theory/concrete_category/bundled.lean
apply_nolint category_theory.bundled has_inhabited_instance

Expand Down

0 comments on commit 0f89392

Please sign in to comment.