inhabit — Mathlib

Lean4
/-- `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`.
-/
@[tactic_parser 1000]
public meta def inhabit : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Lean.Elab.Tactic.inhabit 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "inhabit " false✝)
        (ParserDescr.unary✝ `optional
          (ParserDescr.unary✝ `atomic
            (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ident) (ParserDescr.symbol✝ " : ")))))
      (ParserDescr.cat✝ `term 0))
Похожие утверждения