doc blame linter and prop

Stream: mathlib4

[Patrick Massot]

The doc blame linter asks for documentation of prop-valued fields of structure, for instance in

class CompleteSemilatticeSup (α : Type _) extends PartialOrder α, SupSet α where
  le_supₛ : ∀ s, ∀ a ∈ s, a ≤ supₛ s
  supₛ_le : ∀ s a, (∀ b ∈ s, b ≤ a) → supₛ s ≤ a

Is this expected behavior? Do we really want this? I don't see how I could write a docstring that is easier to read than the actual definition.

[Mario Carneiro]

I don't see how I could write a docstring that is easier to read than the actual definition.

If you think this then you have been formalizing too much. Not everyone reads symbols as easily as this, especially if they use weird lean-specific notations like sup_s

[Patrick Massot]

I did end up writing docstrings in https://github.com/leanprover-community/mathlib4/pull/1053/commits/c13f6c732af9de743f301f5653748f04ae3e9fad. But the main question is about the inconsistency of requiring no docstring for theorems but requiring them for prop-valued fields.

[Mario Carneiro]

the prop-valued fields are still defs though, presumably they also trip the def-lemma linter unless it has a special exemption