Theorems · Definition

List.headI

{α : Type u_1} → [Inhabited α] → List α → α

The head of a list, or the default element of the type is the list is nil.

Defined in

Mathlib.Data.List.Defs

Cited by

42 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

Inhabited