Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - chore(scripts): update nolints.txt #8245

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore(scripts): update nolints.txt #8245

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 0 additions & 6 deletions scripts/nolints.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,6 @@
import .all
run_cmd tactic.skip

-- category_theory/category/Kleisli.lean
apply_nolint category_theory.Kleisli doc_blame unused_arguments has_inhabited_instance
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

-- computability/partrec.lean
apply_nolint computable doc_blame
apply_nolint computable₂ doc_blame
Expand Down
1 change: 0 additions & 1 deletion scripts/style-exceptions.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ src/analysis/normed_space/bounded_linear_maps.lean : line 10 : ERR_MOD : Module
src/category_theory/adjunction/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/adjunction/fully_faithful.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/category_theory/adjunction/limits.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/category/Kleisli.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/category_theory/endomorphism.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/category_theory/epi_mono.lean : line 15 : ERR_MOD : Module docstring missing, or too late
src/category_theory/eq_to_hom.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Expand Down