structure Lean.Try.Config : Type

Configuration for try?.

• main : Bool

  If main is true, all functions in the current module are considered for function induction, unfolding, etc.

• name : Bool

  If name is true, all functions in the same namespace are considered for function induction, unfolding, etc.

• targetOnly : Bool

  If targetOnly is true, try? collects information using the goal target only.

• max : Nat

  Maximum number of suggestions.

• missing : Bool

  If missing is true, allows the construction of partial solutions where some of the subgoals are sorry.

• only : Bool

  If only is true, generates solutions using grind only and simp only.

• harder : Bool

  If harder is true, more expensive tactics and operations are tried.

• merge : Bool

  If merge is true, it tries to compress suggestions such as

  induction a
  · grind only [= f]
  · grind only [→ g]
  

  as

  induction a <;> grind only [= f, → g]
  

• wrapWithBy : Bool

  If wrapWithBy is true, suggestions are wrapped with by for term mode usage.

def Lean.Try.instInhabitedConfig.default : Config

instance Lean.Try.instInhabitedConfig : Inhabited Config

def Lean.Parser.Tactic.tryTrace : ParserDescr

def Lean.Parser.Tactic.attemptAll : ParserDescr

Helper internal tactic for implementing the tactic try?.

def Lean.Parser.Tactic.attemptAllPar : ParserDescr

Helper internal tactic for implementing the tactic try? with parallel execution.

def Lean.Parser.Tactic.firstPar : ParserDescr

Helper internal tactic for implementing the tactic try? with parallel execution, returning first success.

def Lean.Parser.Tactic.tryResult : ParserDescr

Helper internal tactic used to implement evalSuggest in try?

def Lean.Parser.Command.registerTryTactic : ParserDescr

register_try?_tactic tac registers a tactic tac as a suggestion generator for the try? tactic.

An optional priority can be specified with register_try?_tactic (priority := 500) tac. Higher priority generators are tried first. The default priority is 1000.

def «tactic∎» : Lean.ParserDescr

∎ (typed as \qed) is a macro that expands to try? in tactic mode.

def «term∎» : Lean.ParserDescr

∎ (typed as \qed) is a macro that expands to by try? (wrapWithBy := true) in term mode. The wrapWithBy config option causes suggestions to be prefixed with by.

@[inline]

def Lean.Try.Marker {α : Sort u} (a : α) : α

Marker for try?-solved subproofs in exact? +try? suggestions. When exact? uses try? as a discharger, it wraps the proof in this marker so that the unexpander can replace it with (by try?) in the suggestion.

def Lean.Try.markerUnexpander : PrettyPrinter.Unexpander