List.{u} (α : Type u) : Type u

List α is the type of ordered lists with elements of type α. It is implemented as a linked list.

List α is isomorphic to Array α, but they are useful for different things:

• List α is easier for reasoning, and Array α is modeled as a wrapper around List α

• List α works well as a persistent data structure, when many copies of the tail are shared. When the value is not shared, Array α will have better performance because it can do destructive updates.

Constructors

• nil.{u} {α : Type u} : List α

  [] is the empty list.

• cons.{u} {α : Type u} (head : α) (tail : List α) : List α

  If a : α and l : List α, then cons a l, or a :: l, is the list whose first element is a and with l as the rest of the list.