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
Instances For

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

    Equations
    Instances For

      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

        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