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

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.

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

@[reducible, inline]

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

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

@[reducible, inline]

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

@[implicit_reducible]

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

@[reducible, inline]

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

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.

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

Entry in the try suggestion registry

• name : Name
• prio : Nat

@[implicit_reducible]

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

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

@[reducible, inline]

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

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

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

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.

@[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.evalAndSuggest (tk : Syntax) (tac : TSyntax `tactic) (originalMaxHeartbeats : Nat) (config : Try.Config := { }) : TacticM Unit

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.evalTryTrace : Tactic

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

def Lean.Elab.Tactic.Try.elabEmptyByAsTry : Term.TermElab

When the by body is empty and tactic.tryOnEmptyBy is set, run try? for its informational side effect (the "Try this" suggestions) and then delegate to the normal by elaborator so the empty body still produces an unsolved-goals error. The implicit mode must not change elaboration behavior beyond emitting messages. Disabled when errToSorry is false (nested in a combinator like first), or when try? infrastructure is not yet available (e.g. while building the prelude).

We register a second builtin_term_elab for byTactic (rather than folding the gate-and-dispatch into elabByTactic directly) because Lean.Elab.Tactic.Try already imports Lean.Elab.BuiltinTerm, so the try? infrastructure can't be referenced from BuiltinTerm.lean without breaking the dependency direction. The gate in elabByTactic skips this elaborator (via throwUnsupportedSyntax) when the try? path doesn't apply. This could be cleaned up later, e.g. via a registered handler ref in BuiltinTerm.lean populated by Try.lean.