# Documentation

Mathlib.Tactic.Inhabit

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) :

Derives Inhabited α from Nonempty α with Classical.choice

Equations
• = { default := Classical.ofNonempty }

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

Equations

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 : ) (term : Lean.Syntax) :

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.