"Try this" data types

This defines the data types used in constructing "try this" widgets for suggestion-providing tactics and inline error-message hints, as well as basic infrastructure for generating info trees and widget content there from.

Code action information

Suggestion data

inductive Lean.Meta.Tactic.TryThis.SuggestionText : Type

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.

• tsyntax {kind : SyntaxNodeKind} : TSyntax kind → SuggestionText

  TSyntax kind used as suggested replacement text in the infoview. Note that while TSyntax is in general parameterized by a list of SyntaxNodeKinds, we only allow one here; this unambiguously guides pretty-printing.

• string : String → SuggestionText

  A raw string to be used as suggested replacement text in the infoview.

def Lean.Meta.Tactic.TryThis.instInhabitedSuggestionText.default : SuggestionText

instance Lean.Meta.Tactic.TryThis.instInhabitedSuggestionText : Inhabited SuggestionText

instance Lean.Meta.Tactic.TryThis.instToMessageDataSuggestionText : ToMessageData SuggestionText

instance Lean.Meta.Tactic.TryThis.instCoeHeadTSyntaxConsSyntaxNodeKindNilSuggestionText {kind : SyntaxNodeKind} : CoeHead (TSyntax kind) SuggestionText

instance Lean.Meta.Tactic.TryThis.instCoeStringSuggestionText : Coe String SuggestionText

def Lean.Meta.Tactic.TryThis.SuggestionStyle : Type

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.

instance Lean.Meta.Tactic.TryThis.instInhabitedSuggestionStyle : Inhabited SuggestionStyle

instance Lean.Meta.Tactic.TryThis.instToJsonSuggestionStyle : ToJson SuggestionStyle

@[deprecated "`SuggestionStyle` is not used anymore." (since := "2025-08-14")]

def Lean.Meta.Tactic.TryThis.SuggestionStyle.error (decorated : Bool := true) : SuggestionStyle

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

@[deprecated "`SuggestionStyle` is not used anymore." (since := "2025-08-14")]

def Lean.Meta.Tactic.TryThis.SuggestionStyle.warning (decorated : Bool := true) : SuggestionStyle

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

@[deprecated "`SuggestionStyle` is not used anymore." (since := "2025-08-14")]

def Lean.Meta.Tactic.TryThis.SuggestionStyle.success : SuggestionStyle

Style as a success.

@[deprecated "`SuggestionStyle` is not used anymore." (since := "2025-08-14")]

def Lean.Meta.Tactic.TryThis.SuggestionStyle.asHypothesis : SuggestionStyle

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

@[deprecated "`SuggestionStyle` is not used anymore." (since := "2025-08-14")]

def Lean.Meta.Tactic.TryThis.SuggestionStyle.asInaccessible : SuggestionStyle

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

@[deprecated "`SuggestionStyle` is not used anymore." (since := "2025-08-14")]

def Lean.Meta.Tactic.TryThis.SuggestionStyle.value (t : Float) (showValueInHoverText : Bool := true) : SuggestionStyle

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).

structure Lean.Meta.Tactic.TryThis.Suggestion : Type

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.

• suggestion : SuggestionText

  Text to be used as a replacement via a code action.

• preInfo? : Option String

  Optional info to be printed immediately before replacement text in a widget.

• postInfo? : Option String

  Optional info to be printed immediately after replacement text in a widget.

• style? : Option SuggestionStyle

  Optional style specification for the suggestion. If none (the default), the suggestion is styled as a text link. Otherwise, the suggestion can be styled as:

  • a status: .error, .warning, .success
  • a hypothesis name: .asHypothesis, .asInaccessible
  • a variable color: .value (t : Float), which draws from a red-yellow-green gradient, with red at 0.0 and green at 1.0.

  See SuggestionStyle for details.

  Note that this property is used only by the "try this" widget; it is ignored by the inline hint widget.

• messageData? : Option MessageData

  How to represent the suggestion as MessageData. This is used only in the text of the widget diagnostic. If none, we use suggestion. Use toMessageData to render a Suggestion in this manner.

• toCodeActionTitle? : Option (String → String)

  How to construct the text that appears in the lightbulb menu from the suggestion text. If none, we use fun ppSuggestionText => "Try this: " ++ ppSuggestionText. Only the pretty-printed suggestion : SuggestionText is used here.

def Lean.Meta.Tactic.TryThis.instInhabitedSuggestion.default : Suggestion

instance Lean.Meta.Tactic.TryThis.instInhabitedSuggestion : Inhabited Suggestion

instance Lean.Meta.Tactic.TryThis.instToMessageDataSuggestion : ToMessageData Suggestion

instance Lean.Meta.Tactic.TryThis.instCoeSuggestionTextSuggestion : Coe SuggestionText Suggestion

structure Lean.Meta.Tactic.TryThis.TryThisInfo : Type

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

• edit : Lsp.TextEdit

  Suggestion edit as it will be applied to the editor document.

• codeActionTitle : String

  Title of the code action that is displayed in the code action selection dialog.

• suggestion : Suggestion

  Original suggestion that this TryThisInfo was derived from. Stored so that meta-code downstream can extract the suggestions produced by a tactic from the InfoTree.

instance Lean.Meta.Tactic.TryThis.instTypeNameTryThisInfo : TypeName TryThisInfo

Formatting

def Lean.Meta.Tactic.TryThis.getIndentAndColumn (map : FileMap) (range : Syntax.Range) : Nat × Nat

Yields (indent, column) given a FileMap and a Lean.Syntax.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.

opaque Lean.Meta.Tactic.TryThis.format.inputWidth : Lean.Option Nat

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

def Lean.Meta.Tactic.TryThis.getInputWidth (o : Options) : Nat

Get the input width specified in the options

def Lean.Meta.Tactic.TryThis.SuggestionText.pretty : SuggestionText → CoreM Format

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.

def Lean.Meta.Tactic.TryThis.SuggestionText.prettyExtra (s : SuggestionText) (w : Option Nat := none) (indent column : Nat := 0) : CoreM String

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.

def Lean.Meta.Tactic.TryThis.Suggestion.pretty (s : Suggestion) (w : Option Nat := none) (indent column : Nat := 0) : CoreM String

def Lean.Meta.Tactic.TryThis.Suggestion.processEdit (s : Suggestion) (range : Syntax.Range) : CoreM Lsp.TextEdit