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 considere for function induction, unfolding, etc.

• lib : Bool

  If lib is true, uses libSearch results.

• targetOnly : Bool

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

instance Lean.Try.instInhabitedConfig : Inhabited Config

Equations

• Lean.Try.instInhabitedConfig = { default := { main := default, name := default, lib := default, targetOnly := default } }

def Lean.Parser.Tactic.tryTrace : ParserDescr

Equations

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