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]
  

def Lean.Try.instInhabitedConfig.default : Config

Equations

• Lean.Try.instInhabitedConfig.default = { main := default, name := default, targetOnly := default, max := default, missing := default, only := default, harder := default, merge := default }

instance Lean.Try.instInhabitedConfig : Inhabited Config

Equations

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

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.