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.

instance Lean.Try.instInhabitedConfig : Inhabited Config

Equations

• Lean.Try.instInhabitedConfig = { default := Lean.Try.instInhabitedConfig.default }

def Lean.Try.instInhabitedConfig.default : Config

Equations

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

def Lean.Parser.Tactic.tryTrace : ParserDescr

Equations

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

def Lean.Parser.Tactic.attemptAll : ParserDescr

Helper internal tactic for implementing the tactic try?.

Equations

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

def Lean.Parser.Tactic.tryResult : ParserDescr

Helper internal tactic used to implement evalSuggest in try?

Equations

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

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.

Equations

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

def «tactic∎» : Lean.ParserDescr

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

Equations

• «tactic∎» = Lean.ParserDescr.node `«tactic∎» 1024 (Lean.ParserDescr.nonReservedSymbol "∎" false)

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.

Equations

• «term∎» = Lean.ParserDescr.node `«term∎» 1024 (Lean.ParserDescr.symbol "∎")