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.

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 : TypeType} [inst : Monad m] [inst : Lean.MonadLog m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadOptions m] (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