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.

structure Lean.Elab.Tactic.Try.Context : Type

• mvarId : MVarId
• config : Try.Config
• tk : Syntax

instance Lean.Elab.Tactic.instOrElseM {α : Type} : OrElse (Lean.Elab.Tactic.M✝ α)

Equations

• Lean.Elab.Tactic.instOrElseM = { orElse := fun (a : Lean.Elab.Tactic.M✝ α) (b : Unit → Lean.Elab.Tactic.M✝ α) (ctx : Lean.Elab.Tactic.Try.Context) => a ctx <|> b () ctx }

inductive Lean.Elab.Tactic.TacticKind : Type

• exec : TacticKind
• suggestion : TacticKind
• error : TacticKind

def Lean.Elab.Tactic.evalTryTrace : Tactic

Equations

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