"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 Std.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 Std.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 Std.Tactic.TryThis.instTypeNameTryThisInfo : TypeName Std.Tactic.TryThis.TryThisInfo

Equations

• Std.Tactic.TryThis.instTypeNameTryThisInfo = Std.Tactic.TryThis.inst✝

def Std.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 Std.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 Std.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 Std.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.

def Std.Tactic.TryThis.inputWidth : Nat

The default maximum width of an ideal line in source code, 100 is the current convention.

Equations

• Std.Tactic.TryThis.inputWidth = 100

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

An option allowing the user to customize the ideal input width, this controls output format when the output is intended to be copied back into a lean file

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

Get the input width specified in the options

Equations

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

Suggestion data

inductive Std.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 → Std.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 → Std.Tactic.TryThis.SuggestionText

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

instance Std.Tactic.TryThis.instInhabitedSuggestionText : Inhabited Std.Tactic.TryThis.SuggestionText

Equations

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

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

Equations

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

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

Equations

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

instance Std.Tactic.TryThis.instCoeStringSuggestionText : Coe String Std.Tactic.TryThis.SuggestionText

Equations

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

def Std.Tactic.TryThis.SuggestionText.pretty : Std.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

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

def Std.Tactic.TryThis.SuggestionText.prettyExtra (s : Std.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.

def Std.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

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

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

Style as a success.

Equations

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

def Std.Tactic.TryThis.SuggestionStyle.asHypothesis : Std.Tactic.TryThis.SuggestionStyle

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

Equations

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

def Std.Tactic.TryThis.SuggestionStyle.asInaccessible : Std.Tactic.TryThis.SuggestionStyle

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

Equations

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

def Std.Tactic.TryThis.SuggestionStyle.value (t : Float) (showValueInHoverText : optParam Bool true) : Std.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 Std.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 : Std.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 Std.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 Std.Tactic.TryThis.instInhabitedSuggestion : Inhabited Std.Tactic.TryThis.Suggestion

Equations

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

def Std.Tactic.TryThis.Suggestion.toJsonAndInfoM (s : Std.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 Std.Tactic.TryThis.instToMessageDataSuggestion : Lean.ToMessageData Std.Tactic.TryThis.Suggestion

Equations

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

instance Std.Tactic.TryThis.instCoeSuggestionTextSuggestion : Coe Std.Tactic.TryThis.SuggestionText Std.Tactic.TryThis.Suggestion

Equations

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

def Std.Tactic.TryThis.delabToRefinableSuggestion (e : Lean.Expr) : Lean.MetaM Std.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 Std.Tactic.TryThis.addSuggestion (ref : Lean.Syntax) (s : Std.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 Std.Tactic.TryThis.addSuggestions (ref : Lean.Syntax) (suggestions : Array Std.Tactic.TryThis.Suggestion) (origSpan? : optParam (Option Lean.Syntax) none) (header : optParam String "Try these:") (style? : optParam (Option Std.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 Std.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 Std.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 Std.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 Std.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 Std.Tactic.TryThis.addHaveSuggestion (ref : Lean.Syntax) (h? : Option Lean.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 Std.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.