"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

def Lean.Meta.Tactic.TryThis.tryThisWidget : Lean.Widget.Module

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.

Code action

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.

• range : Lean.Lsp.Range

  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.

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

Equations

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

def Lean.Meta.Tactic.TryThis.tryThisProvider : Lean.Server.CodeActionProvider

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.

Formatting

def Lean.Meta.Tactic.TryThis.getIndentAndColumn (map : Lean.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.

def Lean.Meta.Tactic.TryThis.replaceMVarsByUnderscores {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (s : Lean.Syntax) : m Lean.Syntax

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.

def Lean.Meta.Tactic.TryThis.delabToRefinableSyntax (e : Lean.Expr) : Lean.MetaM Lean.Term

Delaborate e into syntax suitable for use by refine.

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 : Lean.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

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 : Lean.SyntaxNodeKind} → Lean.TSyntax kind → Lean.Meta.Tactic.TryThis.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 → Lean.Meta.Tactic.TryThis.SuggestionText

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.Tactic.TryThis.SuggestionText.pretty : Lean.Meta.Tactic.TryThis.SuggestionText → Lean.CoreM Lean.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 : Lean.Meta.Tactic.TryThis.SuggestionText) (w : optParam (Option Nat) none) (indent : optParam Nat 0) (column : optParam Nat 0) : Lean.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.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

def Lean.Meta.Tactic.TryThis.SuggestionStyle.error (decorated : optParam Bool true) : Lean.Meta.Tactic.TryThis.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.

def Lean.Meta.Tactic.TryThis.SuggestionStyle.warning (decorated : optParam Bool true) : Lean.Meta.Tactic.TryThis.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.

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

Style as a success.

Equations

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

def Lean.Meta.Tactic.TryThis.SuggestionStyle.asHypothesis : Lean.Meta.Tactic.TryThis.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")]

def Lean.Meta.Tactic.TryThis.SuggestionStyle.asInaccessible : Lean.Meta.Tactic.TryThis.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")]

def Lean.Meta.Tactic.TryThis.SuggestionStyle.value (t : Float) (showValueInHoverText : optParam Bool true) : Lean.Meta.Tactic.TryThis.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 : Lean.Meta.Tactic.TryThis.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 Lean.Meta.Tactic.TryThis.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.

• messageData? : Option Lean.MessageData

  How to represent the suggestion as MessageData. This is used only in the info 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.

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

Equations

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

def Lean.Meta.Tactic.TryThis.Suggestion.toJsonAndInfoM (s : Lean.Meta.Tactic.TryThis.Suggestion) (w : optParam (Option Nat) none) (indent : optParam Nat 0) (column : optParam Nat 0) : Lean.CoreM (Lean.Json × String × Option String)

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.

instance Lean.Meta.Tactic.TryThis.instToMessageDataSuggestion : Lean.ToMessageData Lean.Meta.Tactic.TryThis.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 Lean.Meta.Tactic.TryThis.SuggestionText Lean.Meta.Tactic.TryThis.Suggestion

Equations

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

def Lean.Meta.Tactic.TryThis.delabToRefinableSuggestion (e : Lean.Expr) : Lean.MetaM Lean.Meta.Tactic.TryThis.Suggestion

Delaborate e into a suggestion suitable for use by refine.

Equations

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

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) : Lean.MetaM Unit

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 String → String 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.

def Lean.Meta.Tactic.TryThis.addSuggestions (ref : Lean.Syntax) (suggestions : Array Lean.Meta.Tactic.TryThis.Suggestion) (origSpan? : optParam (Option Lean.Syntax) none) (header : optParam String "Try these:") (style? : optParam (Option Lean.Meta.Tactic.TryThis.SuggestionStyle) none) (codeActionPrefix? : optParam (Option String) none) : Lean.MetaM Unit

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 String → String 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.

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) : Lean.MetaM Unit

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.

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) : Lean.MetaM Unit

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.

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) : Lean.MetaM Unit

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.

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) : Lean.MetaM Unit

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.

def Lean.Meta.Tactic.TryThis.addHaveSuggestion (ref : Lean.Syntax) (h? : Option Lake.Name) (t? : Option Lean.Expr) (e : Lean.Expr) (origSpan? : optParam (Option Lean.Syntax) none) : Lean.Elab.TermElabM Unit

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

Equations

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

def Lean.Meta.Tactic.TryThis.addRewriteSuggestion (ref : Lean.Syntax) (rules : List (Lean.Expr × Bool)) (type? : optParam (Option Lean.Expr) none) (loc? : optParam (Option Lean.Expr) none) (origSpan? : optParam (Option Lean.Syntax) none) : Lean.Elab.TermElabM Unit

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

Equations

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