Documentation

Lean.Meta.Tactic.TryThis

"Try this" support #

This implements a mechanism for tactics to print a message saying Try this: <suggestion>, where <suggestion> is a link to a replacement tactic. Users can either click on the link in the suggestion (provided by a widget), or use a code action which applies the suggestion.

Raw widget #

This is a widget which is placed by TryThis.addSuggestion and TryThis.addSuggestions.

When placed by addSuggestion, it says Try this: <replacement> where <replacement> is a link which will perform the replacement.

When placed by addSuggestions, it says:

Try these:
  • <replacement1>
  • <replacement2>
  • <replacement3>
  • ...

where <replacement*> is a link which will perform the replacement.

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

    Code action #

    A packet of information about a "Try this" suggestion that we store in the infotree for the associated code action to retrieve.

    • The textual range to be replaced by one of the suggestions.

    • suggestionTexts : Array (String × Option String)

      A list of suggestions for the user to choose from. Each suggestion may optionally come with an override for the code action title.

    • codeActionPrefix? : Option String

      The prefix to display before the code action for a "Try this" suggestion if no custom code action title is provided. If not provided, "Try this: " is used.

    Instances For

      This is a code action provider that looks for TryThisInfo nodes and supplies a code action to apply the replacement.

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

        Formatting #

        Yields (indent, column) given a FileMap and a String.Range, where indent is the number of spaces by which the line that first includes range is initially indented, and column is the column range starts at in that line.

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

          Replace subexpressions like ?m.1234 with ?_ so it can be copy-pasted.

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

            Delaborate e into syntax suitable for use by refine.

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

              An option allowing the user to customize the ideal input width. Defaults to 100. This option controls output format when the output is intended to be copied back into a lean file

              Suggestion data #

              Text to be used as a suggested replacement in the infoview. This can be either a TSyntax kind for a single kind : SyntaxNodeKind or a raw String.

              Instead of using constructors directly, there are coercions available from these types to SuggestionText.

              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                • Lean.Meta.Tactic.TryThis.instCoeHeadTSyntaxConsSyntaxNodeKindNilSuggestionText = { coe := Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax }

                Pretty-prints a SuggestionText as a Format. If the SuggestionText is some TSyntax kind, we use the appropriate pretty-printer; strings are coerced to Formats as-is.

                Equations
                Instances For

                  Pretty-prints a SuggestionText as a String and wraps with respect to the pane width, indentation, and column, via Format.prettyExtra. If w := none, then w := getInputWidth (← getOptions) is used. Raw Strings are returned as-is.

                  Equations
                  Instances For

                    Style hooks for Suggestions. See SuggestionStyle.error, .warning, .success, .value, and other definitions here for style presets. This is an arbitrary Json object, with the following interesting fields:

                    • title: the hover text in the suggestion link
                    • className: the CSS classes applied to the link
                    • style: A Json object with additional inline CSS styles such as color or textDecoration.
                    Equations
                    Instances For

                      Style as an error. By default, decorates the text with an undersquiggle; providing the argument decorated := false turns this off.

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

                        Style as a warning. By default, decorates the text with an undersquiggle; providing the argument decorated := false turns this off.

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

                          Style the same way as a hypothesis appearing in the infoview.

                          Equations
                          Instances For

                            Style the same way as an inaccessible hypothesis appearing in the infoview.

                            Equations
                            Instances For

                              Draws the color from a red-yellow-green color gradient with red at 0.0, yellow at 0.5, and green at 1.0. Values outside the range [0.0, 1.0] are clipped to lie within this range.

                              With showValueInHoverText := true (the default), the value t will be included in the title of the HTML element (which appears on hover).

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

                                Holds a suggestion for replacement, along with preInfo and postInfo strings to be printed immediately before and after that suggestion, respectively. It also includes an optional MessageData to represent the suggestion in logs; by default, this is none, and suggestion is used.

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

                                  Converts a Suggestion to Json in CoreM. We need CoreM in order to pretty-print syntax.

                                  This also returns a String × Option String consisting of the pretty-printed text and any custom code action title if toCodeActionTitle? is provided.

                                  If w := none, then w := getInputWidth (← getOptions) is used.

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

                                    Delaborate e into a suggestion suitable for use by refine.

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

                                      Widget hooks #

                                      def Lean.Meta.Tactic.TryThis.addSuggestion (ref : Lean.Syntax) (s : Lean.Meta.Tactic.TryThis.Suggestion) (origSpan? : optParam (Option Lean.Syntax) none) (header : optParam String "Try this: ") (codeActionPrefix? : optParam (Option String) none) :

                                      Add a "try this" suggestion. This has three effects:

                                      • An info diagnostic is displayed saying Try this: <suggestion>
                                      • A widget is registered, saying Try this: <suggestion> with a link on <suggestion> to apply the suggestion
                                      • A code action is added, which will apply the suggestion.

                                      The parameters are:

                                      • ref: the span of the info diagnostic
                                      • s: a Suggestion, which contains
                                        • suggestion: the replacement text;
                                        • preInfo?: an optional string shown immediately after the replacement text in the widget message (only)
                                        • postInfo?: an optional string shown immediately after the replacement text in the widget message (only)
                                        • style?: an optional Json object used as the value of the style attribute of the suggestion text's element (not the whole suggestion element).
                                        • messageData?: an optional message to display in place of suggestion in the info diagnostic (only). The widget message uses only suggestion. If messageData? is none, we simply use suggestion instead.
                                        • toCodeActionTitle?: an optional function StringString describing how to transform the pretty-printed suggestion text into the code action text which appears in the lightbulb menu. If none, we simply prepend "Try This: " to the suggestion text.
                                      • origSpan?: a syntax object whose span is the actual text to be replaced by suggestion. If not provided it defaults to ref.
                                      • header: a string that begins the display. By default, it is "Try this: ".
                                      • codeActionPrefix?: an optional string to be used as the prefix of the replacement text if the suggestion does not have a custom toCodeActionTitle?. If not provided, "Try this: " is used.
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        Add a list of "try this" suggestions as a single "try these" suggestion. This has three effects:

                                        • An info diagnostic is displayed saying Try these: <list of suggestions>
                                        • A widget is registered, saying Try these: <list of suggestions> with a link on each <suggestion> to apply the suggestion
                                        • A code action for each suggestion is added, which will apply the suggestion.

                                        The parameters are:

                                        • ref: the span of the info diagnostic
                                        • suggestions: an array of Suggestions, which each contain
                                          • suggestion: the replacement text;
                                          • preInfo?: an optional string shown immediately after the replacement text in the widget message (only)
                                          • postInfo?: an optional string shown immediately after the replacement text in the widget message (only)
                                          • style?: an optional Json object used as the value of the style attribute of the suggestion text's element (not the whole suggestion element).
                                          • messageData?: an optional message to display in place of suggestion in the info diagnostic (only). The widget message uses only suggestion. If messageData? is none, we simply use suggestion instead.
                                          • toCodeActionTitle?: an optional function StringString describing how to transform the pretty-printed suggestion text into the code action text which appears in the lightbulb menu. If none, we simply prepend "Try This: " to the suggestion text.
                                        • origSpan?: a syntax object whose span is the actual text to be replaced by suggestion. If not provided it defaults to ref.
                                        • header: a string that precedes the list. By default, it is "Try these:".
                                        • style?: a default style for all suggestions which do not have a custom style? set.
                                        • codeActionPrefix?: an optional string to be used as the prefix of the replacement text for all suggestions which do not have a custom toCodeActionTitle?. If not provided, "Try this: " is used.
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          def Lean.Meta.Tactic.TryThis.addExactSuggestion (ref : Lean.Syntax) (e : Lean.Expr) (origSpan? : optParam (Option Lean.Syntax) none) (addSubgoalsMsg : optParam Bool false) (codeActionPrefix? : optParam (Option String) none) :

                                          Add an exact e or refine e suggestion.

                                          The parameters are:

                                          • ref: the span of the info diagnostic
                                          • e: the replacement expression
                                          • origSpan?: a syntax object whose span is the actual text to be replaced by suggestion. If not provided it defaults to ref.
                                          • addSubgoalsMsg: if true (default false), any remaining subgoals will be shown after Remaining subgoals:
                                          • codeActionPrefix?: an optional string to be used as the prefix of the replacement text if the suggestion does not have a custom toCodeActionTitle?. If not provided, "Try this: " is used.
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            def Lean.Meta.Tactic.TryThis.addExactSuggestions (ref : Lean.Syntax) (es : Array Lean.Expr) (origSpan? : optParam (Option Lean.Syntax) none) (addSubgoalsMsg : optParam Bool false) (codeActionPrefix? : optParam (Option String) none) :

                                            Add exact e or refine e suggestions.

                                            The parameters are:

                                            • ref: the span of the info diagnostic
                                            • es: the array of replacement expressions
                                            • origSpan?: a syntax object whose span is the actual text to be replaced by suggestion. If not provided it defaults to ref.
                                            • addSubgoalsMsg: if true (default false), any remaining subgoals will be shown after Remaining subgoals:
                                            • codeActionPrefix?: an optional string to be used as the prefix of the replacement text for all suggestions which do not have a custom toCodeActionTitle?. If not provided, "Try this: " is used.
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              def Lean.Meta.Tactic.TryThis.addTermSuggestion (ref : Lean.Syntax) (e : Lean.Expr) (origSpan? : optParam (Option Lean.Syntax) none) (header : optParam String "Try this: ") (codeActionPrefix? : optParam (Option String) none) :

                                              Add a term suggestion.

                                              The parameters are:

                                              • ref: the span of the info diagnostic
                                              • e: the replacement expression
                                              • origSpan?: a syntax object whose span is the actual text to be replaced by suggestion. If not provided it defaults to ref.
                                              • header: a string which precedes the suggestion. By default, it's "Try this: ".
                                              • codeActionPrefix?: an optional string to be used as the prefix of the replacement text if the suggestion does not have a custom toCodeActionTitle?. If not provided, "Try this: " is used.
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                def Lean.Meta.Tactic.TryThis.addTermSuggestions (ref : Lean.Syntax) (es : Array Lean.Expr) (origSpan? : optParam (Option Lean.Syntax) none) (header : optParam String "Try these:") (codeActionPrefix? : optParam (Option String) none) :

                                                Add term suggestions.

                                                The parameters are:

                                                • ref: the span of the info diagnostic
                                                • es: an array of the replacement expressions
                                                • origSpan?: a syntax object whose span is the actual text to be replaced by suggestion. If not provided it defaults to ref.
                                                • header: a string which precedes the list of suggestions. By default, it's "Try these:".
                                                • codeActionPrefix?: an optional string to be used as the prefix of the replacement text for all suggestions which do not have a custom toCodeActionTitle?. If not provided, "Try this: " is used.
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  Add a suggestion for have h : t := e.

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

                                                    Add a suggestion for rw [h₁, ← h₂] at loc.

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