From acedda0dfd5d44e140605c9e9c4ec52f87b3a5c8 Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Tue, 4 Aug 2020 00:36:52 +0000 Subject: [PATCH] chore(scripts): update nolints.txt (#3682) I am happy to remove some nolints for you! --- scripts/nolints.txt | 6 ------ 1 file changed, 6 deletions(-) diff --git a/scripts/nolints.txt b/scripts/nolints.txt index 2c2f1ddadbe0e..744ef6c0dfdd8 100644 --- a/scripts/nolints.txt +++ b/scripts/nolints.txt @@ -1288,9 +1288,6 @@ apply_nolint unique doc_blame -- measure_theory/category/Meas.lean apply_nolint Meas doc_blame --- measure_theory/integration.lean -apply_nolint measure_theory.measure.with_density doc_blame - -- measure_theory/measurable_space.lean apply_nolint measurable_equiv has_inhabited_instance @@ -1366,9 +1363,6 @@ apply_nolint fixed_points.next_fixed doc_blame apply_nolint fixed_points.prev doc_blame apply_nolint fixed_points.prev_fixed doc_blame --- order/galois_connection.lean -apply_nolint galois_insertion has_inhabited_instance - -- order/lexicographic.lean apply_nolint lex doc_blame