A very simple try? tactic implementation.

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

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

Equations

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

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

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.