# Lean "nonempty" vs "inhabited"

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?

• I find the Lean terminology confusing. In my world it is: nonempty A means $A \to \emptyset$; inhabited A means $\exists x \in A . \top$; and pointed means $\Sigma_{A : \mathsf{Type}} A$, or in fibered form pointed A means $A$. Apr 16, 2022 at 7:25
• @Andrej Bauer, Lean calls $A → ∅$ is_empty A, which seems like the opposite of the meaning you're suggesting. Do you really use "nonempty" to mean "has no elements"?
– Eric
Apr 16, 2022 at 7:51
• Ah yes, sorry about that, I've just returned from England. I should have $(A \to \emptyset) \to \emptyset$, or equivalently $\neg\neg \exists x \in A . \top$. Apr 16, 2022 at 8:01
• @Guy Coder: the relevant lines of the files you link to (both Lean 3, just different versions of it) are equivalent if not identical, so the distinction isn't important.
– Eric
Apr 16, 2022 at 19:22

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.