Documentation

Lean.Meta.Hint

A widget for rendering code action suggestions in error messages. Generally, this widget should not be used directly; instead, use MessageData.hint. Note that this widget is intended only for use within message data; it may not display line breaks properly if rendered as a panel widget.

The props to this widget are of the following form:

{
  "diff": [
    {"type": "unchanged", "text": "h"},
    {"type": "deletion", "text": "ello"},
    {"type": "insertion", "text": "i"}
  ]
}

Note: we cannot add the builtin_widget_module attribute here because that would require importing Lean.Widget.UserWidget, which in turn imports much of Lean.Elab -- the module where we want to be able to use this widget. Instead, we register the attribute post-hoc when we declare the regular "Try This" widget in Lean.Meta.Tactic.TryThis.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    A code action suggestion associated with a hint in a message.

    Refer to TryThis.Suggestion; this extends that structure with a span? field, allowing a single hint to suggest modifications at different locations. If span? is not specified, then the syntax reference provided to MessageData.hint will be used.

    Instances For

      Produces a diff that splits either on characters, tokens, or not at all, depending on the edit distance between the arguments.

      Guarantees that all actions in the output will be maximally grouped; that is, instead of returning #[(.insert, "a"), (.insert, "b")], it will return #[(.insert, "ab")].

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def Lean.Meta.Hint.mkSuggestionsMessage (suggestions : Array Suggestion) (ref : Syntax) (codeActionPrefix? : Option String) :

          Creates message data corresponding to a HintSuggestions collection and adds the corresponding info leaf.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def Lean.MessageData.hint (hint : MessageData) (suggestions : Array Meta.Hint.Suggestion) (ref? : Option Syntax := none) (codeActionPrefix? : Option String := none) :

            Creates a hint message with associated code action suggestions.

            To provide a hint without an associated code action, use MessageData.hint'.

            The arguments are as follows:

            • hint: the main message of the hint, which precedes its code action suggestions.
            • suggestions: the suggestions to display.
            • ref?: if specified, the syntax location for the code action suggestions; otherwise, default to the syntax reference in the monadic state. Will be overridden by the span? field on any suggestions that specify it.
            • codeActionPrefix?: if specified, text to display in place of "Try this: " in the code action label
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For