Zulip Chat Archive
Stream: mathlib4
Topic: Depriming fields
Kyle Miller (Apr 04 2025 at 06:12):
The new Lean release has a feature where you can override the binder kinds for the type's parameters in structure/class fields. For example, I just made mathlib#23656 to deprime the field for CharP.
class _root_.CharP (R : Type*) [AddMonoidWithOne R] (p : ℕ) : Prop where
cast_eq_zero_iff (R p) : ∀ x : ℕ, (x : R) = 0 ↔ p ∣ x
This makes R and p explicit in CharP.cast_eq_zero_iff. They would normally be implicit since they appear in the return type.
The rule is that you can only override the binder kinds for parameters that actually appear in the declaration. There's an error if you try overriding binder kinds for parameters from variables.
(CharP is the class that @Kevin Buzzard mentioned in #lean4 > RFC: adjust argument explicitness on typeclass projections @ 💬)
Edward van de Meent (Apr 04 2025 at 06:40):
Do we want to lint for places that could/should use this? Do we want to add these cases to the technical debt counter?
Eric Wieser (Apr 04 2025 at 07:37):
Is this also possible for constructors? That would let us merge docs#ModuleCat.of and ModuleCat.mk
Kyle Miller (Apr 04 2025 at 07:39):
No, that feature doesn't exist, and I think that would require a change to the kernel (!)
Kim Morrison (Apr 07 2025 at 03:59):
Just generating a list of all primed field names would be a great start.
Yury G. Kudryashov (Apr 07 2025 at 04:02):
Note that fields like *.map_add' shouldn't be unprimed.
Kevin Buzzard (Apr 07 2025 at 06:15):
Yes, one way of finding an approximate list of targets is to search the mathlib3 source code for the [] pattern in structures (I wrote a regex in the lean 4 issue which seemed to be doing the trick)
Robert Maxton (May 01 2025 at 21:30):
Kyle Miller said:
No, that feature doesn't exist, and I think that would require a change to the kernel (!)
I assume the same applies to inductive arms?
Kyle Miller (May 01 2025 at 21:36):
@Robert Maxton Correct, you can't change the implicitness of a type's parameters in a constructor. The next best thing is to define your own pattern using @[match_pattern] to sort of override the constructor.
Eric Wieser (May 02 2025 at 03:00):
Kevin Buzzard said:
Yes, one way of finding an approximate list of targets is to search the mathlib3 source code for the
[]pattern in structures (I wrote a regex in the lean 4 issue which seemed to be doing the trick)
There is an open issue now with a list produced in this way
Robin Carlier (Jun 10 2025 at 15:26):
In #25664, I deprime the fields in Functor.LaxMonoidal and Functor.OplaxMonoidal.
In spoiler below is a quick regex search of all the classes in CategoryTheory that have at least one primed field:
id : file; class ...
If maintainers review the classes in this list and give me a list of those they want to see deprimed, I can work on this.
Robin Carlier (Jun 27 2025 at 11:16):
I’ve been suggested to unprime an other field (CatCommSq.iso') today, so I’ll allow myself to bump the post above.
If maintainers want fields deprimed, at least for CategoryTheory/, I am willing to do the grunt work here provided they do the triage of which ones they want to keep primed and which ones they feel should be unprimed.
Last updated: Dec 20 2025 at 21:32 UTC