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

def Std.Tactic.TryThis.tryThisWidget : Lean.Widget.UserWidgetDefinition

This is a widget which is placed by TryThis.addSuggestion; it says Try this: <replacement> where <replacement> is a link which will perform the replacement.

Equations

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

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.

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.Elab.TermElabM Lean.Term

Delaborate e into an expression suitable for use in 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

def Std.Tactic.TryThis.addSuggestion (ref : Lean.Syntax) {kind : Lean.Name} (suggestion : Lean.TSyntax kind) (suggestionForMessage? : optParam (Option Lean.MessageData) none) (origSpan? : optParam (Option Lean.Syntax) none) (extraMsg : optParam String "") : 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 Apply 'Try this' is added, which will apply the suggestion.

The parameters are:

• ref: the span of the info diagnostic
• suggestion: the replacement syntax
• suggestionForMessage?: the message to display in the info diagnostic (only). The widget message uses only suggestion. If not provided, suggestion is used in both places.
• origSpan?: a syntax object whose span is the actual text to be replaced by suggestion. If not provided it defaults to ref.
• extraMsg: an extra piece of message text to apply to the widget message (only).

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

Add a 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.

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) : Lean.Elab.TermElabM 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.

Equations

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