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?
$\begingroup$
$\endgroup$
4
1 Answer
$\begingroup$
$\endgroup$
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 Ameans $A \to \emptyset$;inhabited Ameans $\exists x \in A . \top$; andpointedmeans $\Sigma_{A : \mathsf{Type}} A$, or in fibered formpointed Ameans $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$