Nonempty types #
This file proves a few extra facts about
Nonempty, which is defined in core Lean.
Main declarations #
Classical.choice, lifts a (
Nonempty instance to a (
Classical.inhabited_of_nonempty already exists, in
Init/Classical.lean, but the assumption is not a type class argument,
which makes it unsuitable for some applications.