From 1f8f3a0363fae885a09e582fff8aa4b0f74a9402 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 22 Jun 2026 16:00:07 +0200 Subject: [PATCH 1/2] feat(naming): update naming conventions for Prop-valued classes --- templates/contribute/naming.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/templates/contribute/naming.md b/templates/contribute/naming.md index a29c4153e..25be0feeb 100644 --- a/templates/contribute/naming.md +++ b/templates/contribute/naming.md @@ -525,13 +525,18 @@ and "let $G$ be a group and let $H$ be a normal subgroup" is written and `Normal H` are not extra data, but are extra assumptions on data we have already. Mathlib currently strives towards the following naming convention for these `Prop`-valued -classes. If the class is a noun then its name should begin with `Is`. If however is it an adjective +classes. If the class is a noun (or noun phrase) then its name should begin with `Is`. If however is it an adjective then its name does not need to begin with an `Is`. So for example `IsNormal` would be acceptable for the "normal subgroup" typeclass, but `Normal` is also fine; we might say "assume the subgroup `H` is normal" in informal language. However `IsTopologicalRing` is preferred for the "topological ring" typeclass, as we do not say "assume the ring `R` is topological" informally. +If the predicate is referring to data other than the explicit argument, +then the prefix `Has` may be used instead of the prefix `Is`. +Examples: `Filter.HasBasis`, `Function.HasLeftInverse`, `HasLimit` (for a functor in category theory), +`HasCompactSupport` (`IsCompactlySupportedFunction` would also follow this naming scheme, but is very long). + ### Unexpanded and expanded forms of functions The multiplication of two functions `f` and `g` can be denoted equivalently as From 5a8aa6522b41c5f199fa33458a08c398913a6d0e Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 22 Jun 2026 16:11:42 +0200 Subject: [PATCH 2/2] fix --- templates/contribute/naming.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/templates/contribute/naming.md b/templates/contribute/naming.md index 25be0feeb..464161e3e 100644 --- a/templates/contribute/naming.md +++ b/templates/contribute/naming.md @@ -533,7 +533,7 @@ preferred for the "topological ring" typeclass, as we do not say "assume the rin topological" informally. If the predicate is referring to data other than the explicit argument, -then the prefix `Has` may be used instead of the prefix `Is`. +then the prefix `Has` may be used instead of the prefix `Is`, if that sounds more natural. Examples: `Filter.HasBasis`, `Function.HasLeftInverse`, `HasLimit` (for a functor in category theory), `HasCompactSupport` (`IsCompactlySupportedFunction` would also follow this naming scheme, but is very long).