"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

Equations

• Lean.Meta.Tactic.TryThis.instInhabitedSuggestionText.default = Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax default

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

Equations

• Lean.Meta.Tactic.TryThis.instInhabitedSuggestionText = { default := Lean.Meta.Tactic.TryThis.instInhabitedSuggestionText.default }

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

Equations

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

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

Equations

• Lean.Meta.Tactic.TryThis.instCoeHeadTSyntaxConsSyntaxNodeKindNilSuggestionText = { coe := Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax }

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

Equations

• Lean.Meta.Tactic.TryThis.instCoeStringSuggestionText = { coe := Lean.Meta.Tactic.TryThis.SuggestionText.string }

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.

Equations

• Lean.Meta.Tactic.TryThis.SuggestionStyle = Lean.Json

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

Equations

• Lean.Meta.Tactic.TryThis.instInhabitedSuggestionStyle = Lean.instInhabitedJson

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

Equations

• Lean.Meta.Tactic.TryThis.instToJsonSuggestionStyle = Lean.instToJsonJson

@[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.

Equations

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

@[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.

Equations

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

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

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

Style as a success.

Equations

• Lean.Meta.Tactic.TryThis.SuggestionStyle.success = Lean.Json.mkObj [("className", Lean.Json.str "information pointer dim")]

@[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.

Equations

• Lean.Meta.Tactic.TryThis.SuggestionStyle.asHypothesis = Lean.Json.mkObj [("className", Lean.Json.str "goal-hyp pointer dim")]

@[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.

Equations

• Lean.Meta.Tactic.TryThis.SuggestionStyle.asInaccessible = Lean.Json.mkObj [("className", Lean.Json.str "goal-inaccessible pointer dim")]

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.Tactic.TryThis.instInhabitedSuggestion = { default := Lean.Meta.Tactic.TryThis.instInhabitedSuggestion.default }

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

Equations

• Lean.Meta.Tactic.TryThis.instToMessageDataSuggestion = { toMessageData := fun (s : Lean.Meta.Tactic.TryThis.Suggestion) => s.messageData?.getD (Lean.toMessageData s.suggestion) }

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

Equations

• Lean.Meta.Tactic.TryThis.instCoeSuggestionTextSuggestion = { coe := fun (t : Lean.Meta.Tactic.TryThis.SuggestionText) => { suggestion := t } }

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

Equations

• Lean.Meta.Tactic.TryThis.instTypeNameTryThisInfo = Lean.Meta.Tactic.TryThis.inst✝

Formatting

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

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.

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

Equations

• Lean.Meta.Tactic.TryThis.getInputWidth o = Lean.Option.get o Lean.Meta.Tactic.TryThis.format.inputWidth

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.

Equations

• (Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax stx).pretty = Lean.PrettyPrinter.ppCategory kind stx.raw
• (Lean.Meta.Tactic.TryThis.SuggestionText.string s).pretty = pure (Std.Format.text s)

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.

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Meta.Tactic.TryThis.SuggestionText.string s_1).prettyExtra w indent column = pure s_1

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

Equations

• s.pretty w indent column = s.suggestion.prettyExtra w indent column

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

Equations

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