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

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

• Lean.Elab.Tactic.Try.withNonTerminal x = withReader (fun (c : Lean.Elab.Tactic.Try.Ctx) => { root := c.root, terminal := false, config := c.config }) x

opaque Lean.Elab.Tactic.Try.tryTacticElabAttribute : KeyedDeclsAttribute TryTactic

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

@[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) (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

Main code

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

Equations

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