Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#3969)
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 29, 2020
1 parent 4ccbb51 commit 2d3530d
Showing 1 changed file with 0 additions and 8 deletions.
8 changes: 0 additions & 8 deletions scripts/nolints.txt
Original file line number Diff line number Diff line change
Expand Up @@ -140,10 +140,8 @@ apply_nolint category_theory.limits.cofan.mk doc_blame
apply_nolint category_theory.limits.fan doc_blame
apply_nolint category_theory.limits.fan.mk doc_blame
apply_nolint category_theory.limits.pi.lift doc_blame
apply_nolint category_theory.limits.pi.map doc_blame
apply_nolint category_theory.limits.pi.π doc_blame
apply_nolint category_theory.limits.sigma.desc doc_blame
apply_nolint category_theory.limits.sigma.map doc_blame
apply_nolint category_theory.limits.sigma.ι doc_blame

-- category_theory/monad/adjunction.lean
Expand Down Expand Up @@ -1444,9 +1442,6 @@ apply_nolint ext_param_type doc_blame
apply_nolint get_ext_subject doc_blame
apply_nolint opt_minus doc_blame
apply_nolint saturate_fun doc_blame
apply_nolint tactic.ext doc_blame
apply_nolint tactic.ext1 doc_blame
apply_nolint tactic.try_intros doc_blame

-- tactic/fin_cases.lean
apply_nolint tactic.expr_list_to_list_expr doc_blame
Expand Down Expand Up @@ -1477,12 +1472,9 @@ apply_nolint tactic.interactive.revert_all doc_blame
apply_nolint tactic.generalize_proofs doc_blame

-- tactic/interactive.lean
apply_nolint tactic.interactive.apply_iff_congr_core doc_blame
apply_nolint tactic.interactive.collect_struct doc_blame
apply_nolint tactic.interactive.collect_struct' doc_blame
apply_nolint tactic.interactive.compact_decl_aux doc_blame
apply_nolint tactic.interactive.congr_core' doc_blame
apply_nolint tactic.interactive.convert_to_core doc_blame
apply_nolint tactic.interactive.field doc_blame
apply_nolint tactic.interactive.format_names doc_blame
apply_nolint tactic.interactive.get_current_field doc_blame
Expand Down

0 comments on commit 2d3530d

Please sign in to comment.