Defines the `inhabit α`

tactic, which tries to construct an `Inhabited α`

instance,
constructively or otherwise.

Derives `Inhabited α`

from `Nonempty α`

with `Classical.choice`

## Equations

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

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 }

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

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