Attach usage suggestions to set definitions

[SReichelt]

When defining a set (construction or operator), optionally provide suggestions on how to use or construct an element of that set.

• Usage suggestions should apply to variables in the current context (including variables that are not directly applicable at the given location). In certain cases, they should also extend the library tree; see below.
• Construction suggestions should apply whenever a term of the given set is expected.

Currently, the following suggestions would be desirable:

• Usage (using data provided for Add decomposition hints #36):
  • Properties: "has property"
  • Relations: "related"
  • Functions and operations: "value"
  • Any structure: "Carrier"
    • This will solve the case "Let G be a group, g in G".
    • To avoid confusion, it should also extend to definitions in the library. I.e. it should become possible to directly enter something like "Let g in S_42".
    • Do we need any additional convenience functionality for explicit structure definitions, similarly to type classes or canonical structures in other provers?
• Construction:
  • Wherever a number is required, it should be possible to enter this number directly. This is strongly connected to Directly allow numbers as terms #74.
  • If there is only a single constructor with a single parameter, and this constructor can be applied to a variable in the current context, that should become a suggestion.
  • If there is only a single constructor and that constructor contains a binding (e.g. property, relation, function, operator), there should be an immediate way to select a predicate or operator in a way that makes the special rendering due to Replace simple macros with special rendering #68 transparent (see outdated issue Automatically select macros to convert library items to terms #9).
  • If a macro exists that produces an element of the given set, that macro should be suggested. Low priority because currently, this would only provide suggestions for tuples and matrices of fixed size (which are rare), if numbers are already handled differently.

Suggestions that are based on variables could show up directly in the list of variables.