Depriming fields

Stream: mathlib4

[Kyle Miller]

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]

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]

Is this also possible for constructors? That would let us merge docs#ModuleCat.of and ModuleCat.mk

[Kyle Miller]

No, that feature doesn't exist, and I think that would require a change to the kernel (!)

[Kim Morrison]

Just generating a list of all primed field names would be a great start.

[Yury G. Kudryashov]

Note that fields like *.map_add' shouldn't be unprimed.

[Kevin Buzzard]

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]

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]

@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]

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