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

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

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

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.

Equations

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