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

source
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 }

Instances For

source
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 := ⋯ }

Instances For

source
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.

Instances For

source
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.

Instances For