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 : Type → Type}
[inst : Monad m]
[inst : Lean.MonadQuotation m]
(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 : 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
- Std.Tactic.TryThis.addSuggestion origStx suggestion = Lean.logInfoAt origStx (Lean.toMessageData "" ++ Lean.toMessageData suggestion ++ Lean.toMessageData "")
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
- Std.Tactic.TryThis.addTermSuggestion origTerm e = do let __do_lift ← Std.Tactic.TryThis.delabToRefinableSyntax e Std.Tactic.TryThis.addSuggestion origTerm __do_lift.raw