A very simple try? tactic implementation.

opaque Lean.Elab.Tactic.debug.tactic.try.onlyUserSuggestions : Lean.Option Bool

def Lean.Elab.Tactic.elabTryConfig (cfg : Syntax) (init : Try.Config := { }) (logExceptions : Bool := true) : TacticM Try.Config

Equations

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

evalSuggest is a evalTactic variant that returns suggestions after executing a tactic built using combinators such as first, attempt_all, <;>, ;, and try.

def Lean.Elab.Tactic.Try.checkTactic (savedState : SavedState) (tac : TSyntax `tactic) : TacticM Unit

Executes tac in the saved state. This function is used to validate a tactic before suggesting it.

Equations

• Lean.Elab.Tactic.Try.checkTactic savedState tac = do let currState ← Lean.saveState savedState.restore tryFinally (Lean.Elab.Tactic.evalTactic tac.raw) currState.restore

def Lean.Elab.Tactic.Try.evalSuggestExact : TacticM (TSyntax `tactic)

Equations

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

@[reducible, inline]

abbrev Lean.Elab.Tactic.Try.TacticResult (α : Type) : Type

Equations

• Lean.Elab.Tactic.Try.TacticResult α = EStateM.Result Lean.Exception Lean.Elab.Tactic.SavedState α

structure Lean.Elab.Tactic.Try.Ctx : Type

• root : TSyntax `tactic
• terminal : Bool
• config : Try.Config
• originalMaxHeartbeats : Nat

@[reducible, inline]

abbrev Lean.Elab.Tactic.Try.TryTacticM (α : Type) : Type

Equations

• Lean.Elab.Tactic.Try.TryTacticM = ReaderT Lean.Elab.Tactic.Try.Ctx Lean.Elab.Tactic.TacticM

@[reducible, inline]

abbrev Lean.Elab.Tactic.Try.TryTactic : Type

Equations

• Lean.Elab.Tactic.Try.TryTactic = (Lean.TSyntax `tactic → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic))

@[instance_reducible]

instance Lean.Elab.Tactic.Try.instMonadBacktrackSavedStateTryTacticM : MonadBacktrack SavedState TryTacticM

Equations

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

@[reducible, inline]

abbrev Lean.Elab.Tactic.Try.withNonTerminal {α : Type} (x : TryTacticM α) : TryTacticM α

Equations

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

opaque Lean.Elab.Tactic.Try.tryTacticElabAttribute : KeyedDeclsAttribute TryTactic

User-extensible try suggestion generators

@[reducible, inline]

abbrev Lean.Elab.Tactic.Try.TrySuggestionGenerator : Type

A user-defined generator that proposes tactics for try? to attempt. Takes the goal MVarId and collected info, returns array of tactics to try.

Equations

• Lean.Elab.Tactic.Try.TrySuggestionGenerator = (Lean.MVarId → Lean.Meta.Try.Info → Lean.MetaM (Array (Lean.TSyntax `tactic)))

structure Lean.Elab.Tactic.Try.TrySuggestionEntry : Type

Entry in the try suggestion registry

• name : Name
• prio : Nat

@[instance_reducible]

instance Lean.Elab.Tactic.Try.instInhabitedTrySuggestionEntry : Inhabited TrySuggestionEntry

Equations

• Lean.Elab.Tactic.Try.instInhabitedTrySuggestionEntry = { default := Lean.Elab.Tactic.Try.instInhabitedTrySuggestionEntry.default }

opaque Lean.Elab.Tactic.Try.trySuggestionExtension : SimpleScopedEnvExtension TrySuggestionEntry (Array TrySuggestionEntry)

Environment extension for user try suggestion generators (supports local scoping)

def Lean.Elab.Tactic.Try.elabRegisterTryTactic : Command.CommandElab

Elaborate register_try?_tactic command

Equations

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

@[reducible, inline]

abbrev Lean.Elab.Tactic.Try.focus {α : Type} (x : TryTacticM α) : TryTacticM α

Equations

• Lean.Elab.Tactic.Try.focus x ctx = Lean.Elab.Tactic.focus (x ctx)

def Lean.Elab.Tactic.Try.observing {α : Type} (x : TryTacticM α) : TryTacticM (TacticResult α)

Equations

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

def Lean.Elab.Tactic.Try.withOriginalHeartbeats {α : Type} (x : TryTacticM α) : TryTacticM α

Executes a tactic with heartbeat management:

• Restores the original maxHeartbeats limit (recorded at try? start)
• Gives the tactic a fresh heartbeat budget via withCurrHeartbeats
• Catches heartbeat exceptions and converts them to regular errors

Equations

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

def Lean.Elab.Tactic.Try.withUnlimitedHeartbeats {α : Type} {m : Type → Type} [Monad m] [MonadWithReaderOf Core.Context m] [MonadControlT CoreM m] (x : m α) : m α

Executes code with unlimited heartbeats (maxHeartbeats set to 0). Used by try? infrastructure itself so it doesn't timeout while testing tactics.

Equations

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

@[extern lean_eval_suggest_tactic]

opaque Lean.Elab.Tactic.Try.evalSuggest : TryTactic

@[builtin_try_tactic] registrations for the built-in combinators and trace wrappers.

evalSuggest dispatcher.

evalAndSuggest frontend

def Lean.Elab.Tactic.Try.evalAndCollectSuggestions (tac : TSyntax `tactic) (originalMaxHeartbeats : Nat) (config : Try.Config := { }) : TacticM (Array Meta.Tactic.TryThis.Suggestion)

Like evalAndSuggest, but returns the suggestion array instead of emitting it.

Equations

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

def Lean.Elab.Tactic.Try.evalAndSuggest (tk : Syntax) (tac : TSyntax `tactic) (originalMaxHeartbeats : Nat) (config : Try.Config := { }) : TacticM Unit

Equations

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

Helper functions

grind tactic syntax generator based on collected information.

Other generators

Function induction generators

Vanilla induction generators

Main code

def Lean.Elab.Tactic.Try.elabTryCore (tk : Syntax) (config : Try.Config) (footer : MessageData := MessageData.nil) : TacticM Unit

Core implementation of try?: focus, collect info, build tactic, evaluate and suggest. tk is the syntax token where "Try this:" appears. The optional footer is appended to the suggestions message (only when wrapWithBy := true).

Public so that the autoTry linter (Lean.Elab.Tactic.AutoTry) can drive try? from outside the normal try? syntax entry point.

Equations

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

def Lean.Elab.Tactic.Try.collectTryCoreSuggestions (config : Try.Config := { }) : TacticM (Array (TSyntax `tactic))

Like elabTryCore, but returns the suggestion array (as raw tactic syntaxes) instead of emitting "Try this:" messages. Used by the autoTry linter, which formats and emits the suggestions itself so they can be rendered as append-to-tactic-sequence edits.

Equations

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

def Lean.Elab.Tactic.Try.evalTryTrace : Tactic

Equations

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

def Lean.Elab.Tactic.Try.evalTryTraceWith : Tactic

Equations

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