Search categories for constants with opaque (lemmas, etc) and transparent (definition, ...) bodies

[Villetaneuse]

Is your feature request related to a problem?

It should be possible to search for

• "logical" constants (Lemmas, Theorems, ...)
• "definitional" constants (Definitions, Fixpoints, ...)
  without knowing which keyword was used.
  At this point the is:logical_kind of Search requires that the user has this information.

Proposed solution

I propose (following @JasonGross suggestion here) we add the
is:Qed and is:Defined in Search queries.

Alternative solutions

My initial idea was to add another Search keyword like kind:Transparent and kind:Opaque.
What is already possible at this point is to Search ... [is:Lemma | is:Theorem] and Search ... [is:Definition | is:Fixpoint] (if/after PR #18983 is merged), which is quite verbose and not really equivalent.

Additional context

No response

[herbelin]

I would say that Transparent and Opaque refers to the current status of a Defined constant for the non-kernel parts while Qed and Defined would refer to the kernel status of the constant. So both pairs of keys make sense I would say.

[JasonGross]

I would say that Transparent and Opaque refers to the current status of a Defined constant for the non-kernel parts

The kernel's heuristics care about Transparent and Opaque though. Maybe it makes sense to generalize this to:

1. Search for constants with a given range / set of Strategy levels (subsumes Transparent and Opaque for kernel things)
2. Search for things that are Hint Transparent and Hint Opaque for a given hint database