Skip to content

Commit 5cc2e72

Browse files
grunwegBergschaf
authored andcommitted
chore: rename delaborators to match naming convention (leanprover-community#39822)
Change from delab_foo to delabFoo (as these are Type-valued, not Prop-valued, so should be lowerCamelCase by naming rule 4). This should not need deprecations, as presumably these delaborators are never called directly. Found by the linter added in leanprover-community#34519.
1 parent 69a57b2 commit 5cc2e72

3 files changed

Lines changed: 2 additions & 4 deletions

File tree

Mathlib/Data/Set/Notation.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ If the `Set.Notation` namespace is open, sets of a subtype coerced to the ambien
4646
represented with `↑`.
4747
-/
4848
@[scoped delab app.Set.image]
49-
meta def delab_set_image_subtype : Delab := whenPPOption getPPCoercions do
49+
meta def delabSetImageSubtype : Delab := whenPPOption getPPCoercions do
5050
let #[α, _, f, _] := (← getExpr).getAppArgs | failure
5151
guard <| f.isAppOfArity ``Subtype.val 2
5252
let some _ := α.coeTypeSet? | failure

Mathlib/Util/Delaborators.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -171,7 +171,7 @@ end existential
171171
open Lean Lean.PrettyPrinter.Delaborator
172172

173173
/-- Delaborator for `∉`. -/
174-
@[app_delab Not] def delab_not_in := whenPPOption Lean.getPPNotation do
174+
@[app_delab Not] def delabNotIn := whenPPOption Lean.getPPNotation do
175175
let #[f] := (← SubExpr.getExpr).getAppArgs | failure
176176
guard <| f.isAppOfArity ``Membership.mem 5
177177
let stx₁ ← SubExpr.withAppArg <| SubExpr.withNaryArg 3 delab

scripts/nolints.json

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@
44
["defsWithUnderscore", "cfcₙHom_of_cfcHom"],
55
["defsWithUnderscore", "commandSuppress_compilation"],
66
["defsWithUnderscore", "decidableEq_of_subsingleton"],
7-
["defsWithUnderscore", "delab_not_in"],
87
["defsWithUnderscore", "equiv_linearIndependent"],
98
["defsWithUnderscore", "exists_delab"],
109
["defsWithUnderscore", "finiteness_nonterminal"],
@@ -458,7 +457,6 @@
458457
["defsWithUnderscore", "Set.Icc.convexComb_assoc_coeff₁'"],
459458
["defsWithUnderscore", "Set.Icc.convexComb_assoc_coeff₂"],
460459
["defsWithUnderscore", "Set.Icc.convexComb_assoc_coeff₂'"],
461-
["defsWithUnderscore", "Set.Notation.delab_set_image_subtype"],
462460
["defsWithUnderscore", "Set.powersetCard.addActionHom_of_embedding"],
463461
["defsWithUnderscore", "Set.powersetCard.addActionHom_singleton"],
464462
["defsWithUnderscore", "Set.powersetCard.mulActionHom_compl"],

0 commit comments

Comments
 (0)