In the init/logic.lean file of the Lean 3 standard library, nonempty
and inhabited
are defined. It seems like these two classes are very similar - you can instantiate either of them given an element of the type. In what situations do you use one over the other?
1 Answer
The difference between nonempty
and inhabited
is that nonempty A : Prop
but inhabited A : Sort (max 1 u)
(if A : Sort u
). This makes inhabited A
isomorphic as a type to A
, while nonempty A
is the propositional truncation of A
, equivalent to ∃ x : A, true
. To extract a value from inhabited A
is inhabited.default
, but extracting a value from a proof of nonempty A
is the axiom of choice and is noncomputable
.
Generally, you should use nonempty A
if you only need the "mere fact" that A
is not empty, while inhabited A
is used if you need to access a specific default value for totalizing a function or so. Mathlib has a linter to ensure that you don't use inhabited
in place of nonempty
for proving theorems unless you need it in the statement of the theorem.
nonempty A
means $A \to \emptyset$;inhabited A
means $\exists x \in A . \top$; andpointed
means $\Sigma_{A : \mathsf{Type}} A$, or in fibered formpointed A
means $A$. $\endgroup$is_empty A
, which seems like the opposite of the meaning you're suggesting. Do you really use "nonempty" to mean "has no elements"? $\endgroup$