Structures · Lean core

Inhabited

Inhabited α is a typeclass that says that α has a designated element, called (default : α). This is sometimes referred to as a "pointed type". This class is used by functions that need to return a value of the type when called "out of domain". For example, Array.get! arr i : α returns a value of type α when arr : Array α, but if i is not in range of the array, it reports a panic message, but this does not halt the program, so it must still return a value of type α (and in fact this is required for logical consistency), so in this case it returns default.

Defined in: Init.Prelude
Shape: One type argument · adds default

Open in Mathlib docs