Proposition fields result in `def`s not `theorem`s

[eric-wieser]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

When declaring a structure, all the projections are generated as defs even though morally they should sometimes be thought of as theorems. Specifically, fields of type h : P where P : Prop would be more natural as theorems, as this matches the intended use of theorem elsewhere.

Context

This impacts the docBlame linter in Std, which declares that defs should have docstrings (because their type alone doesn't describe their function) but theorems need not.
For now, we are having to work around this for the special case of projections in std4#269.

Steps to Reproduce

structure AtLeastThirtySeven where
  val : Nat
  le : 37 ≤ val

theorem AtLeastThirtySeven.lt (x : AtLeastThirtySeven) : 36 < x.val := x.le

Expected behavior: AtLeastThirtySeven.le and AtLeastThirtySeven.lt should both be theorems (or at least, there should be some way to request that they both be).

Actual behavior: AtLeastThirtySeven.le is a def

Versions

leanprover/lean4:v4.1.0-rc1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.