12.16. Linked Lists🔗

Planned Content

  • Representation at compile time and run time

  • API reference

  • Literal syntax

  • Constructor/pattern syntax

Tracked at issue #108

🔗inductive type
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.