A very simple try? tactic implementation.

def Lean.Elab.Tactic.elabTryConfig : Syntax → 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 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

def Lean.Elab.Tactic.Try.instInhabitedTrySuggestionEntry.default : TrySuggestionEntry

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

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