Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#3704)
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 Aug 6, 2020
1 parent 9d3c709 commit f8fd0c3
Showing 1 changed file with 0 additions and 9 deletions.
9 changes: 0 additions & 9 deletions scripts/nolints.txt
Expand Up @@ -120,12 +120,6 @@ apply_nolint category_theory.Kleisli.comp_def unused_arguments
apply_nolint category_theory.Kleisli.id_def unused_arguments
apply_nolint category_theory.Kleisli.mk doc_blame has_inhabited_instance

-- category_theory/category/default.lean
apply_nolint category_theory.category_struct doc_blame
apply_nolint category_theory.epi doc_blame
apply_nolint category_theory.has_hom doc_blame
apply_nolint category_theory.mono doc_blame

-- category_theory/endomorphism.lean
apply_nolint category_theory.Aut doc_blame has_inhabited_instance
apply_nolint category_theory.End has_inhabited_instance
Expand Down Expand Up @@ -2081,10 +2075,7 @@ apply_nolint topological_space.open_nhds.inclusion_map_iso doc_blame
apply_nolint topological_space.open_nhds.map doc_blame

-- topology/category/Top/opens.lean
apply_nolint topological_space.opens.map_comp doc_blame
apply_nolint topological_space.opens.map_id doc_blame
apply_nolint topological_space.opens.map_iso doc_blame
apply_nolint topological_space.opens.to_Top doc_blame

-- topology/category/TopCommRing.lean
apply_nolint TopCommRing has_inhabited_instance
Expand Down

0 comments on commit f8fd0c3

Please sign in to comment.