Documentation for the different ways to control reducibility

[nielsvoss]

Lean has three different ways to control reducibility: the ConstantKind, annotations, and ReducibilityHints. These all do different things, and even worse, the commands that interact with them are inconsistent (for example, abbrev affects the annotations and reducibility hints while opaque affects the ConstantKind. Mathlib's irreducible_def is a little confusing as well). See the explanation here:

#lean4 > def vs theorem in Lean.ConstantInfo @ 💬

I personally found this very unintuitive, and I was wondering if this should be documented somewhere? (If needed, I could write some of the documentation in a couple of weeks.)