Defines the inhabit α tactic, which tries to construct an Inhabited α instance, constructively or otherwise.

@[implicit_reducible]

noncomputable def Lean.Elab.Tactic.nonempty_to_inhabited (α : Sort u_1) : Nonempty α → Inhabited α

Derives Inhabited α from Nonempty α with Classical.choice.

Equations

• Lean.Elab.Tactic.nonempty_to_inhabited α x✝ = { default := Classical.ofNonempty }

@[implicit_reducible]

def Lean.Elab.Tactic.nonempty_prop_to_inhabited (α : Prop) (α_nonempty : Nonempty α) : Inhabited α

Derives Inhabited α from Nonempty α without Classical.choice assuming α is of type Prop.

Equations

• Lean.Elab.Tactic.nonempty_prop_to_inhabited α α_nonempty = { default := ⋯ }

def Lean.Elab.Tactic.inhabit : ParserDescr

inhabit α tries to derive a Nonempty α instance and then uses it to make an Inhabited α instance. If the target is a Prop, this is done constructively. Otherwise, it uses Classical.choice.

Equations

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

def Lean.Elab.Tactic.evalInhabit (goal : MVarId) (h_name : Option Ident) (term : Syntax) : TacticM MVarId

evalInhabit takes in the MVarId of the main goal, runs the core portion of the inhabit tactic, and returns the resulting MVarId

Equations

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