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

@[instance_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

@[instance_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.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.

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.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.

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.

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

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