# Documentation

Std.Tactic.TryThis

# Stub for try-this support #

Lean 4 does not yet support code actions to present tactic suggestions in the editor. This file contains a preliminary API that tactics can call to show suggestions.

def Std.Tactic.TryThis.replaceMVarsByUnderscores {m : } [inst : ] [inst : ] (s : 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.

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 {m : } [inst : ] [inst : ] [inst : ] [inst : ] (origStx : Lean.Syntax) (suggestion : Lean.Syntax) :

Add a "try this" suggestion. (TODO: this depends on code action support)

Equations

Add a exact e or refine e suggestion. (TODO: this depends on code action support)

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

Add a term suggestion. (TODO: this depends on code action support)

Equations