"Try this" support

This implements a mechanism for tactics to print a message saying Try this: , where 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: where 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.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:
• A widget is registered, saying Try this: with a link on 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.