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

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 }

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 := Lean.Elab.Tactic.nonempty_prop_to_inhabited.proof_1 α α_nonempty }

def Lean.Elab.Tactic.inhabit : Lean.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 : Lean.MVarId) (h_name : Option Lean.Ident) (term : Lean.Syntax) : Lean.Elab.Tactic.TacticM Lean.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.