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.

source
ink
def Std.Tactic.TryThis.replaceMVarsByUnderscores {m : Type → Type} [inst : Monad m] [inst : 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.
source
ink
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.
source
ink
def Std.Tactic.TryThis.addSuggestion {m : Type → Type} [inst : Monad m] [inst : Lean.MonadLog m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadOptions m] (origStx : Lean.Syntax) (suggestion : Lean.Syntax) :
m Unit

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

Equations
source
ink
def Std.Tactic.TryThis.addExactSuggestion (origTac : Lean.Syntax) (e : Lean.Expr) :
Lean.Elab.TermElabM Unit

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.
source
ink
def Std.Tactic.TryThis.addTermSuggestion (origTerm : Lean.Syntax) (e : Lean.Expr) :
Lean.Elab.TermElabM Unit

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

Equations